6.4.10.1. Мотивация

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

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.10.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
• Multiplicity и его продвинутые конструкторы данных (см. LinearTypes)
• LiftedRep (см. Полиморфизм представлений)
• RuntimeRep и его продвинутые конструкторы данных (см. Полиморфизм представлений)
• Levity и его продвинутые конструкторы данных (см. Полиморфизм представлений)
• VecCount и его продвинутые конструкторы данных
• VecElem и его продвинутые конструкторы данных

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

6.4.10.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.10.4. Литералы на уровне типов

DataKinds позволяет использовать числовые и строковые литералы на уровне типов. Для получения дополнительной информации см. Литералы на уровне типов.

6.4.10.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.10.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.10.7. Типы данных и синонимы типов

Расширение 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