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

TypeData

Since:

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