Импортирована ли аннотация% hint / Dec и автоаннотация? - PullRequest
Новая
       26

Импортирована ли аннотация% hint / Dec и автоаннотация?

1 голос
/ 23 апреля 2019

У меня есть тип данных, который зависит от предиката P: a -> Type, что означает, что некоторые из его конструкторов данных имеют неявный P x в качестве аргумента.Я бы хотел, чтобы idris могла автоматически сделать вывод, что это неявно.Для этого я аннотировал неявное ключевое слово auto и написал функцию isP: (x: a) -> Dec (P x) с аннотацией% hint перед объявлением типа.А именно, что-то вроде: 

module P

P : a -> Type

%hint
isP : (x : a) -> Dec (P x)

и в отдельном файле 

module Main

import P

data Foo : Type where
  Bar : (x : a) -> .{auto prf : P x} -> Foo

Тем не менее, я не могу объявить значения указанного типа Foo, потому что Идрис утверждает, что он не может вывестиprf.

Это потому, что prf имеет тип P x вместо Dec (P x) или потому, что флаг подсказки% не импортируется?

В любом случае, как я могу получитьИдрис, чтобы использовать значение Dec, чтобы попытаться найти неявное?

1 Ответ

2 голосов
/ 23 апреля 2019

Флаг %hint импортируется, как вы, наверное, думаете, потому что Dec (P x) отличается от P x.

Хотя есть хитрость, вы можете использовать этот тип данных: 

data IsYes : prop -> Type where
  SoTrue : IsYes (Yes prop)

(в основном вы определяете тип, который содержит Yes для данного свойства), а затем вы можете использовать default вместо auto, чтобы проверить, содержит ли свойство: 

data Foo : Type where
  Bar : (x : a) -> .{default SoTrue prf : IsYes (isP x)} -> Foo

Примечание: с этим трюком вам даже больше не нужно %hint, вы просто проверяете результат isP во время компиляции.

...