Определение типа с помощью рекурсивной функции Тип -> Тип - PullRequest
Новая
       7

Определение типа с помощью рекурсивной функции Тип -> Тип

2 голосов
/ 09 января 2020

В Idris обычно List определяется следующим образом: 

data List a = Nil | (::) a (List a)

Но я хотел попробовать определить List без data, используя рекурсивную функцию Type -> Type: 

List' : Type -> Type
List' a = Either () (a, List' a)

Компилируется, но я не могу сопоставить случаи Either. Например, если я определю 

isEmpty : List' a -> Bool
isEmpty (Left _) = True
isEmpty (Right _) = False

, компилятор скажет: 

When checking left hand side of isEmpty:
When checking an application of Main.isEmpty:
        Type mismatch between
                Either a1 b (Type of Left l)
        and
                List' a (Expected type)

Таким образом, средство проверки типов, похоже, не расширяет List' a в свое определение Either _ _. Кажется, что рекурсивный вызов в определении типа отключает проверку типов - если я вместо этого определю List' следующим образом: 

List' a = Either () (a, ())

, тогда определение isEmpty скомпилируется нормально. (Но, конечно, это больше не список.)

Я хотел бы знать следующее:

  • Почему именно это не работает? Есть ли способ проверить, что происходит внутри проверки типов?
  • Есть ли способ заставить этот тип определения типа работать? Или у нас есть для использования data?
...