Блог

Я занимаюсь некоторыми разработками в Идрисе и столкнулся со следующей проблемой. Допустим, у нас есть 3 вектора:

 xs : Vect len  a
ys : Vect len  a
zs : Vect len' a
 

и скажем, у нас тоже есть

 samelen : len = len' 
 

Наконец, мы также имеем следующие равенства:

 xsys : xs = ys

yszs : ys = zs
 

В первом равенстве мы имеем равенство для типа Vect len a, а во втором — для Vect len’a. Теперь мы хотим установить:

 xsza : xs = zs
 

Мне было нелегко заставить это работать. В частности, trans нуждается в равенстве между одними и теми же типами, но здесь это не так. Как здесь можно использовать транзитивность для достижения xsza?

Почему, конечно:

 xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       len = len' ->
       xs = ys -> ys = zs ->
       xs = zs
xszs {A} {len} {len'=len} xs ys zs Refl = trans
 

Я думаю, важно знать, что это в основном должно быть функцией. Вы не можете использовать sameLen доказательство для замены len на len' в типах объектов, которые уже находятся в области видимости. То есть, если бы все ваши подписи типов были верхнего уровня, Idris никогда не смог бы в этом убедиться zs : Vect len a . Вы должны использовать вспомогательную функцию. В приведенной выше функции len' сопоставляется с len , оправдывается сопоставлением с Refl , перед введением zs переменной. Вы можете возразить, что это явно неверно, что zs и предшествует Refl аргументу, но, поскольку Idris — это общий язык, компилятору разрешено упростить вам жизнь, неявно переупорядочивая абстракцию, сопоставление и все такое прочее. По сути, непосредственно перед Refl сопоставлением, перед zs введением вводится тип цели (zs : Vect len' A) -> xs = ys -> ys = zs -> xs = zs , но совпадение переписывает его (zs : Vect len A) -> ?etc и zs вводится с более приятным типом.

Обратите внимание, что на len = len' самом деле это просто не нужно. Это работает:

 xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       xs = ys -> ys = zs -> xs = zs
xszs {A} {len} {len'=len} xs xs xs Refl Refl = Refl
 

Или даже

 xszs : {A : Type} -> {len, len' : Nat} ->
       (xs, ys : Vect len A) -> (zs : Vect len' A) ->
       xs = ys -> ys = zs -> xs = zs
xszs xs ys zs = trans