6.4.13. Объявления данных на уровне типов

TypeData

С версии:

9.6.1

Разрешает объявления type data, которые определяют конструкторы на уровне типов.

Это расширение упрощает программирование на уровне типов (во время компиляции), позволяя использовать аналог объявлений data на уровне типов, например, следующее определение натуральных чисел на уровне типов:

type data Nat = Zero | Succ Nat

Оно аналогично соответствующему объявлению data, за исключением того, что вводимые им конструкторы Zero и Succ относятся к пространству имён конструкторов типов, поэтому их можно использовать в типах, например в типе векторов с индексированием по длине:

data Vec :: Type -> Nat -> Type where
  Nil  :: Vec a Zero
  Cons :: a -> Vec a n -> Vec a (Succ n)

TypeData — это более гибкая альтернатива расширению DataKinds, которое определяет все конструкторы во всех объявлениях data одновременно как конструкторы данных и конструкторы типов.

Объявление type data имеет тот же синтаксис, что и объявление data — обычный алгебраический тип данных или GADT, — с добавлением ключевого слова type в начале, однако оно не может содержать контекст типа данных (даже с расширением DatatypeContexts), помеченные поля, флаги строгости или предложение deriving.

В типах конструкторов разрешены только ограничения равенства, например:

type data P :: Type -> Type -> Type where
  MkP :: (a ~ Natural, b ~~ Char) => P a b

Поскольку объявления type data вводят конструкторы типов, они не допускают конструкторы с такими же именами, как у типов, поэтому следующее объявление недопустимо:

type data T = T     // Invalid

Компилятор отклонит это объявление, поскольку конструктор типа T определён дважды (как определяемый тип данных и как конструктор типа).

Главный конструктор типа в объявлении type data можно определить рекурсивно, как в примере Nat выше, однако его конструкторы нельзя использовать в типах внутри той же взаимно рекурсивной группы объявлений, поэтому следующий вариант запрещён:

type data T f = K (f (K Int))  // Invalid