Экспериментируя с конгом в Idris REPL - PullRequest
Новая
       34

Экспериментируя с конгом в Idris REPL

0 голосов
/ 05 мая 2019

TL; DR: Я хотел бы привести один или два примера использования cong в REPL Idris, чтобы помочь мне лучше понять его.

Общий тип равенства определен концептуальновот так: 

data (=) : a -> b -> Type where
  Refl : x = x

Когда я впервые столкнулся с этим, я был очень смущен синтаксисом.(Я продолжал думать о = как о операторе, а не как о типе.) Но игра с ним в REPL помогла мне понять.Например, мы можем объявить типы для представления ложных равенств: 

λ> 2 + 2 = 5
4 = 5 : Type
λ> 2 = "wombat"
2 = "wombat" : Type

Однако единственным конструктором для = является Refl, и мы можем использовать его только тогда, когда два аргумента равны. 

λΠ> the (4 = 4) Refl
Refl : 4 = 4
λΠ> the (4 = 5) Refl
... type mismatch

Так что теперь я пытаюсь понять cong, экспериментируя с ним в REPL.Функция cong доказывает, что, если два значения равны, применение функции к ним дает равный результат.Я нашел определение. 

  cong : {f : t -> u} -> (a = b) -> f a = f b
  cong Refl = Refl

Так, например, если я определю ... 

λ> :let twoEqTwo = the (2 = 2) Refl
defined

... тогда я ожидал, что смогу показать, что добавление 1 к обоимстороны приводят к другому равенству. 

λΠ> :let ty = (S 2 = S 2)
defined
λΠ> the ty (cong twoEqTwo)
    ...type mismatch

Может кто-нибудь показать мне пример или два использования cong в REPL?

1 Ответ

2 голосов
/ 06 мая 2019

2 имеют неправильный тип. По умолчанию они имеют тип Integer в twoEqTwo, потому что у них нет других ограничений. Видите, без ограничений 2: 

idris> 2
2 : Integer

Тем не менее, в ty вы говорите S 2. S заставляет все это работать в Nat: 

idris> S 2
3 : Nat

Заставьте twoEqTwo работать и в Nat: 

idris> :let twoEqTwo = the (the Nat 2 = 2) Refl
idris> the (S 2 = S 2) twoEqTwo
Refl : 3 = 3

Обратите внимание, что вывод типа может разобраться сам, если вы позволите ему увидеть все выражение: 

idris> the (S 2 = S 2) (cong (the (2 = 2) Refl))
Refl : 3 = 3
...