Idris Dependent Pairs: неожиданное поведение между скомпилированной программой и REPL - PullRequest
Новая
       29

Idris Dependent Pairs: неожиданное поведение между скомпилированной программой и REPL

0 голосов
/ 06 сентября 2018

Практикуя использование зависимых пар в Idris, я столкнулся с неожиданной разницей в поведении между скомпилированными программами и REPL. Следующий тип данных - это то, с чем я тестирую: 

(a : Type ** b : Type ** Arrow a b)

Что должно представлять некоторую связь между типом a и типом b. Учитывая приведенное выше, я хотел бы извлечь термин «доказательство» типа. Я могу сделать это из REPL с DPair.snd $ DPair.snd <some-instance>, и все работает отлично. Однако, если я попытаюсь сделать функцию: 

unwrap : (a ** b ** Arrow a b) -> Arrow a b
unwrap x = DPair.snd $ DPair.snd x

программа скомпилируется, но не удастся, когда я попытаюсь вызвать ее. Возвращенное сообщение об ошибке 

(input): No such variable b

Кто-нибудь сталкивался с этим или знает решение?

1 Ответ

0 голосов
/ 08 сентября 2018

То, чего вы хотите достичь, невозможно. Если вы посмотрите на тип unwrap : (a1 : Type ** b1 : Type ** Arrow a b) -> Arrow a b, то увидите, что он использует тип данных, отличный от (a : Type ** b : Type ** Arrow a b). Это связано с тем, что аргументы a, b заранее определены количественно - задается результирующий тип (который также отличается от случая REPL; там вы не привязаны к аргументам). Так что с :set showimplicit это 

Main.unwrap : {b : Type} -> {a : Type} ->
              (a1 : Type ** b1 : Type ** Main.Arrow a b) ->
              Main.Arrow a b

Это то, что относится к зависимым парам, вы не можете их легко ограничить. Взгляните на Vect.filter : (elem -> Bool) -> Vect len elem -> (p : Nat ** Vect p elem) - если бы у нас была такая функция, как unwrap : (p : Nat ** Vect p elem) -> Vect p elem, нам бы не понадобилась зависимая пара.

Вместо этого функция, которая будет вызывать unwrap, должна будет проверить p и затем обработать Vect соответственно. К сожалению, мы не можем легко проверить типы (по крайней мере, если вы хотите обобщить для всех типов). Так что ваш лучший выбор: не используйте зависимые типы здесь.

...