Почему «нейтральный» не нормализуется до «[]» в моноиде списка?

Следующие определения типов Idris проверяются с помощью Idris 1.3.0:

foo : (xs : List Nat) -> xs = ([] <+> xs)
foo xs = Refl

однако это не так:

foo : (xs : List Nat) -> xs = (neutral <+> xs)
foo xs = Refl

дает следующую ошибку типа:

 When checking right hand side of foo with expected type
         xs = neutral <+> xs

 Type mismatch between
         neutral ++ xs = neutral ++ xs (Type of Refl)
 and
         xs = neutral ++ xs (Expected type)

 Specifically:
         Type mismatch between
                 neutral ++ xs
         and
                 xs

Почему здесь neutral <+> xs не нормализуется до xs?


typeclass type-level-computation idris
person Cactus    schedule 12.10.2018    source источник

Ответы (1)


arrow_upward
1
arrow_downward

neutral будет интерпретироваться как неявный аргумент, поскольку он написан в нижнем регистре и появляется в объявлении типа. Но можно просто указать модуль. :doc neutral дает мне Prelude.Algebra.neutral:

foo : (xs : List Nat) -> xs = (Algebra.neutral <+> xs)
foo xs = Refl
person xash    schedule 12.10.2018
comment
Ааааааа блин, это не первый раз, когда меня сбивает с толку эта ошибка в синтаксисе Идриса... - person Cactus; 12.10.2018