6.4.11.1. Мотивация

В стандартном Haskell имеется богатый язык типов. Типы классифицируют термы и помогают избежать многих распространённых ошибок программирования. Однако язык видов относительно прост: он различает только обычные типы (вид Type) и конструкторы типов (например, вид Type -> Type -> Type). В частности, при использовании расширенных возможностей системы типов, таких как семейства типов (Семейства типов) или GADT (Обобщённые алгебраические типы данных (GADT)), этой простой системы видов недостаточно, и она не позволяет предотвратить простые ошибки. Рассмотрим пример натуральных чисел на уровне типов и векторов с длиной, заданной на уровне типа:

data Ze
data Su n

data Vec :: Type -> Type -> Type where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

Вид Vec — Type -> Type -> Type. Это означает, что, например, Vec Int Char — корректный с точки зрения вида тип, хотя при определении векторов с длиной, заданной на уровне типа, мы подразумеваем не это.

С помощью DataKinds приведённый выше пример можно переписать так:

data Nat = Ze | Su Nat

data Vec :: Type -> Nat -> Type where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

Благодаря улучшенному виду Vec такие конструкции, как Vec Int Char, теперь имеют некорректный вид, и GHC сообщит об ошибке.

6.4.11.2. Обзор

С помощью DataKinds GHC автоматически превращает каждый тип данных в вид, а его конструкторы значений — в конструкторы типов. Следующие типы

data Nat = Zero | Succ Nat

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

data Pair a b = MkPair a b

data Sum a b = L a | R b

порождают следующие виды и конструкторы типов:

Nat :: Type
Zero :: Nat
Succ :: Nat -> Nat

List :: Type -> Type
Nil  :: forall k. List k
Cons :: forall k. k -> List k -> List k

Pair  :: Type -> Type -> Type
MkPair :: forall k1 k2. k1 -> k2 -> Pair k1 k2

Sum :: Type -> Type -> Type
L :: k1 -> Sum k1 k2
R :: k2 -> Sum k1 k2

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

• Конструкторы экземпляров семейств данных пока нельзя промотировать. Теория типов GHC пока не позволяет промотировать семейства данных, поскольку для этого нужны полноценные зависимые типы.

• Конструкторы данных с контекстами нельзя промотировать. Например:

  data Foo :: Type -> Type where
    MkFoo :: Show a => Foo a    -- not promotable
  

Следующие виды и промотированные конструкторы данных можно использовать, даже если DataKinds не включено:

• Type
• TYPE (см. Полиморфизм представления)
• Constraint (см. Вид Constraint)
• CONSTRAINT
• Multiplicity и его промотированные конструкторы данных (см. LinearTypes)
• LiftedRep (см. Полиморфизм представления)
• RuntimeRep и его промотированные конструкторы данных (см. Полиморфизм представления)
• Levity и его промотированные конструкторы данных (см. Полиморфизм представления)
• VecCount и его промотированные конструкторы данных
• VecElem и его промотированные конструкторы данных

Также можно использовать виды, объявленные с помощью type data (см. TypeData), не включая DataKinds.

6.4.11.3. Различение типов и конструкторов

Рассмотрим

data P = MkP    -- 1

data Prom = P   -- 2

На уровне типов имя P будет обозначать тип P (у которого есть конструктор MkP), а не промотированный конструктор данных P вида Prom. Чтобы обратиться к последнему, поставьте перед ним одиночную кавычку: 'P.

Такой синтаксис можно использовать, даже если неоднозначности нет (то есть в области видимости нет типа P).

GHC поддерживает -Wunticked-promoted-constructors, который выдаёт предупреждение, если промотированный конструктор данных записан без кавычки. Начиная с GHC 9.4 это предупреждение больше не включается параметром -Wall; мы больше не рекомендуем по умолчанию использовать кавычки (см. #20531).

Как и в случае с Template Haskell (Синтаксис), GHC не справляется с кавычкой перед конструктором данных, если вторым символом в его имени тоже является кавычка. В таком случае поставьте пробел между кавычкой промоции и конструктором данных:

data T = A'
type S = 'A'   -- ERROR: looks like a character
type R = ' A'  -- OK: promoted `A'`

6.4.11.4. Литералы на уровне типов

DataKinds разрешает использовать числовые и строковые литералы на уровне типов. Подробнее см. Литералы на уровне типов.

6.4.11.5. Промотированные типы списков и кортежей

С помощью DataKinds типы списков и кортежей Haskell нативно промотируются до видов, сохраняя тот же удобный синтаксис на уровне типов, но с добавлением кавычки:

data HList :: [Type] -> Type where
  HNil  :: HList '[]
  HCons :: a -> HList t -> HList (a ': t)

data Tuple :: (Type,Type) -> Type where
  Tuple :: a -> b -> Tuple '(a,b)

foo0 :: HList '[]
foo0 = HNil

foo1 :: HList '[Int]
foo1 = HCons (3::Int) HNil

foo2 :: HList [Int, Bool]
foo2 = ...

Для списков на уровне типов, содержащих два или более элемента, например для сигнатуры foo2 выше, кавычку можно опустить, поскольку смысл однозначен. Однако для списков из одного или нуля элементов (как в foo0 и foo1) кавычка обязательна, поскольку типы [] и [Int] уже имеют значения в Haskell.

6.4.11.6. Промоция экзистенциальных конструкторов данных

Обратите внимание: мы промотируем подходящие экзистенциальные конструкторы данных. Например, рассмотрим следующее:

data Ex :: Type where
  MkEx :: forall a. a -> Ex

Промотируются и тип Ex, и конструктор данных MkEx, причём их полиморфный вид — 'MkEx :: forall k. k -> Ex. Как ни удивительно, можно написать семейство типов, извлекающее элемент из экзистенциального типа на уровне типов:

type family UnEx (ex :: Ex) :: k
type instance UnEx (MkEx x) = x

На первый взгляд UnEx имеет некорректный вид. Возвращаемый вид k не упоминается в аргументах, поэтому может показаться, что экземпляр должен возвращать элемент k для любого k. Однако это не так. Семейство типов UnEx — это семейство типов, индексируемое видом. Возвращаемый вид k является неявным параметром UnEx. Развёрнутые определения выглядят так (неявные параметры обозначены фигурными скобками):

type family UnEx {k :: Type} (ex :: Ex) :: k
type instance UnEx {k} (MkEx @k x) = x

Таким образом, экземпляр срабатывает только тогда, когда неявный параметр UnEx совпадает с неявным параметром MkEx. Поскольку k на самом деле является параметром UnEx, вид не выходит за пределы экзистенциального типа, и приведённый выше код корректен.

См. также #7347.

6.4.11.7. DataKinds и синонимы типов

Расширение DataKinds взаимодействует с синонимами типов следующим образом:

1. В контексте типа: для использования синонима типа, раскрывающегося в тип, для которого иначе потребовалось бы расширение, DataKinds не требуется. Например:

   {-# LANGUAGE DataKinds #-}
   module A where
   
     type MyTrue = 'True
   
   {-# LANGUAGE NoDataKinds #-}
   module B where
   
     import A
     import Data.Proxy
   
     f :: Proxy MyTrue
     f = Proxy
   

   GHC примет сигнатуру типа для f, даже если DataKinds не включено, поскольку промотированный конструктор данных True скрыт под синонимом типа MyTrue. Однако если бы пользователь написал непосредственно Proxy 'True, то потребовалось бы включить DataKinds.

2. В контексте вида: DataKinds применяется ко всем типам, упомянутым в виде, включая раскрытия синонимов типов. Например, рассмотрим следующий модуль:

   module C where
   
     type MyType = Type
     type MySymbol = Symbol
   

   В этом модуле следующие определения будут приняты или отклонены; в них используется Автономные сигнатуры видов и полиморфная рекурсия:

   {-# LANGUAGE NoDataKinds #-}
   module D where
   
     import C
   
     -- ACCEPTED: The kind only mentions Type, which doesn't require DataKinds
     type D1 :: Type -> Type
     data D1 a
   
     -- REJECTED: The kind mentions Symbol, which requires DataKinds to use in
     -- a kind position
     data D2 :: Symbol -> Type
     data D2 a
   
     -- ACCEPTED: The kind mentions a type synonym MyType that expands to
     -- Type, which doesn't require DataKinds
     data D3 :: MyType -> Type
     data D3 a
   
     -- REJECTED: The kind mentions a type synonym MySymbol that expands to
     -- Symbol, which requires DataKinds to use in a kind position
     data D4 :: MySymbol -> Type
     data D4 a