Определение равенства Списков Функция

Question

Type-Driven Development с Идрисом представляет это упражнение:

same_cons : {xs : List a} -> {ys : List a} -> xs = ys -> x :: xs = x :: ys 

Однако, я попытался реализовать с помощью:

data EqList : (xs : List a) -> (ys : List a) -> Type where 
    Same : (xs: List a) -> EqList xs xs 

sameS : (xs : List a) -> (ys : List a) -> (x: a) -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
sameS xs xs x (Same xs) = Same (x :: xs) 

same_cons : {xs : List a} -> {ys : List a} -> (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons {xs} {ys} eq = sameS xs ys _ eq 

Я выводил x в EqList (x :: xs) (x :: ys), потому что я m путают, как получить x, если xs и ys пустые.

Кроме того, вышеуказанные компилирует, но это не удалось, когда я попытался назвать:

*Exercises> same_cons (Same [1,2,3]) 
(input):Can't infer argument x to same_cons 

Answer 1

неявный аргумент x не может быть выведен в вашем случае использования, потому что нет никакой информации в вызове same_cons (Same [1,2,3]), чтобы ограничить его на что угодно. Если вы исправите тип результата, это даст вам выбор x, например.

λΠ> the (EqList [0,1,2,3] [0,1,2,3]) (same_cons (Same [1,2,3])) 
Same [0, 1, 2, 3] : EqList [0, 1, 2, 3] [0, 1, 2, 3] 

поскольку выбор [0,1,2,3] для x:xs унифицирует x с 0.

BTW можно упростить определение same_cons, так как тип этого eq аргумента определяет xs и ys так что вы можете позволить Идрис умозаключениях:

same_cons : (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 
same_cons eq = sameS _ _ _ eq 

Answer 2

Для уточнения о том, как получить x: Все в нижнем регистре в объявление типа будет неявным аргументом, если он еще не является явным. Так

same_cons : {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

такая же, как

same_cons : {a : Type} -> {x : a} -> {xs : List a} -> {ys : List a} -> 
      (eq : EqList xs ys) -> EqList (x :: xs) (x :: ys) 

Вот где x скрывается. Таким образом, вы можете использовать {x} в левой части определения, чтобы получить его. Или просто позвольте Идрису обрабатывать все вещи и использовать определение Cactus. Для будущих проблем с аргументами вы можете использовать :set showimplicits в REPL, чтобы показать вам все неявные аргументы при запросе типов, например. :t same_cons.

И когда Идрис не может вывести значение для неявного аргумента, вы можете помочь ему, давая результирующий тип, как кактус сделали или установить неявный аргумент к значению:

*> same_cons {x=0} (Same [3,2,5]) 
Same [0, 3, 2, 5] : EqList [0, 3, 2, 5] [0, 3, 2, 5]