6.4.14. Полиморфизм по видам

6.4.14.1. Обзор полиморфизма по видам

Рассмотрим вывод вида для

data App f a = MkApp (f a)

В Haskell 98 выведенный вид для App — (Type -> Type) -> Type -> Type. Но он излишне конкретен, поскольку другой подходящий вид Haskell 98 для App — ((Type -> Type) -> Type) -> (Type -> Type) -> Type, где a присваивается вид Type -> Type. Более того, без сигнатур видов (KindSignatures) необходимо использовать фиктивный конструктор, чтобы компилятор Haskell вывел второй вид. При полиморфизме по видам (PolyKinds) GHC выводит для App вид forall k. (k -> Type) -> k -> Type, который является наиболее общим видом.

Таким образом, главное преимущество полиморфизма по видам состоит в том, что теперь мы можем выводить эти наиболее общие виды и использовать App с разными видами:

App Maybe Int   -- `k` is instantiated to Type

data T a = MkT (a Int)    -- `a` is inferred to have kind (Type -> Type)
App T Maybe     -- `k` is instantiated to (Type -> Type)

6.4.14.2. Обзор расширения Type-in-Type

В GHC 8 идея полиморфизма по видам развивается дальше: типы и виды объявляются одним и тем же. В GHC ничто не различает типы и виды. Можно также сказать, что тип Bool и «поднятый вид» Bool на самом деле тождественны. (Обратите внимание: терм True и тип 'True по-прежнему различаются, поскольку первый можно использовать в выражениях, а второй — в типах.) Отсутствие различия между типами и видами характерно для языков с зависимой типизацией. В языках с полноценной зависимой типизацией также устраняется различие между выражениями и типами, но это тема для другого разговора о GHC.

Одно из упрощений, которое становится возможным при объединении типов и видов, заключается в том, что тип Type — это просто Type. Действительно, аксиома Type :: Type может привести к неостанавливающемуся вычислению, но для GHC это не проблема: у нас уже есть другие способы создавать неостанавливающиеся программы как в типах, так и в выражениях. Это решение (как и многие-многие другие) означает, что, несмотря на выразительность системы типов GHC, «доказательство», написанное на Haskell, не является неопровержимым математическим доказательством. GHC гарантирует лишь частичную корректность: если программы компилируются и завершаются, их результаты действительно имеют назначенные им типы. GHC ничего не утверждает о программах, которые не завершаются за конечное время.

Подробнее об этом решении и устройстве GHC можно узнать из статьи, в которой эта система видов представлена для GHC/Haskell.

6.4.14.3. Принципы вывода видов

В общем случае, если включено PolyKinds, GHC пытается вывести для объявления наиболее общий вид. Во многих случаях (например, в объявлении типа данных) правая часть определения задаёт ограничения для вывода вида. Но так бывает не всегда. Рассмотрим

type family F a

В объявлениях семейств типов нет правой части, но GHC всё равно должен вывести вид для F. Поскольку ограничений нет, можно было бы вывести F :: forall k1 k2. k1 -> k2, но это кажется слишком полиморфным. Поэтому GHC по умолчанию присваивает этим полностью неограниченным переменным вида Type, и мы получаем F :: Type -> Type. Тем не менее, с помощью сигнатур видов можно объявить F полиморфным по видам:

type family F1 a                -- F1 :: Type -> Type
type family F2 (a :: k)         -- F2 :: forall k. k -> Type
type family F3 a :: k           -- F3 :: forall k. Type -> k
type family F4 (a :: k1) :: k2  -- F4 :: forall k1 k2. k1 -> k2

Общий принцип таков:

• Если есть правая часть, GHC выводит наиболее полиморфный вид, совместимый с этой правой частью. Примеры: обычные объявления типов данных и GADT, объявления классов. В объявлении класса роль «правой части» выполняют сигнатуры методов класса.
• Если правой части нет, GHC присваивает аргументам и результату вид Type, если сигнатура вида не задаёт иное. Примеры: объявления семейств данных и открытых семейств типов.

Это правило иногда приводит к неожиданным последствиям (см. #10132).

class C a where    -- Class declarations are generalised
                   -- so C :: forall k. k -> Constraint
  data D1 a        -- No right hand side for these two family
  type F1 a        -- declarations, but the class forces (a :: k)
                   -- so   D1, F1 :: forall k. k -> Type

data D2 a   -- No right-hand side so D2 :: Type -> Type
type F2 a   -- No right-hand side so F2 :: Type -> Type

Полиморфизм по видам в объявлении класса делает D1 полиморфным по видам, но не D2; аналогично, F1 и F2.

6.4.14.4. Вывод вида в сигнатурах типов

При проверке вида типа GHC учитывает только то, что записано в этом типе, определяя, как обобщать его вид.

Например, рассмотрим следующие определения (с включённым ScopedTypeVariables):

data Proxy a    -- Proxy :: forall k. k -> Type
p :: forall a. Proxy a
p = Proxy :: Proxy (a :: Type)

GHC сообщает об ошибке: вид a должен быть переменной вида k, а не Type. Причина в том, что, анализируя сигнатуру типа forall a. Proxy a, GHC предполагает, что вид a должен быть обобщён, а не ограничен значением Type. Поэтому определение функции отклоняется: оно конкретнее, чем её сигнатура типа.

6.4.14.5. Явная квантификация по видам

При включённом PolyKinds GHC поддерживает явную квантификацию по видам, как в следующих примерах:

data Proxy :: forall k. k -> Type
f :: (forall k (a :: k). Proxy a -> ()) -> Int

Обратите внимание, что во втором примере есть forall, связывающий как переменную вида k, так и переменную типа a вида k. В общем случае глубина такой вложенной зависимости не ограничена. Однако зависимость должна быть корректно ограничена областью видимости: forall (a :: k) k. ... — ошибка.

6.4.14.6. Вывод порядка переменных в объявлении типа/класса

Между переменными типа, вводимыми в объявлении типа или класса, могут возникать сложные зависимости. Вот пример:

data T a (b :: k) c = MkT (a c)

Проанализировав это объявление, GHC обнаружит, что a и c могут быть полиморфными по видам, где a :: k2 -> Type и c :: k2. Таким образом, мы выводим следующий вид:

T :: forall {k2 :: Type} (k :: Type). (k2 -> Type) -> k -> k2 -> Type

Обратите внимание, что k2 помещается перед k, а k помещается перед a. Также обратите внимание, что здесь k2 записана в фигурных скобках. Как объясняется в разделе TypeApplications (Выведенные и заданные переменные типа), переменные типа и вида, которые GHC обобщает, но которые не записаны в исходной программе, нельзя использовать для видимого применения типа. (Они называются выведенными переменными.) Такие переменные записываются в фигурных скобках.

Общий принцип таков:

• Сначала идут переменные, недоступные для применения типа.
• Затем идут переменные, записанные пользователем и неявно вводимые в область видимости в виде переменной типа.
• Последними идут обычные переменные типа из объявления.
• Переменные, порядок которых пользователь явно не задал, сортируются согласно ScopedSort (Порядок заданных переменных).

В приведённом выше примере с T мы могли бы связать k после a; это не нарушило бы требований к зависимостям. Однако это противоречило бы нашему общему принципу, поэтому k идёт первой.

Иногда такой порядок не соответствует зависимостям. Например:

data T2 k (a :: k) (c :: Proxy '[a, b])

Переменные a и b должны иметь один и тот же вид. Обратите также внимание, что b неявно объявляется в виде c. Следовательно, согласно нашему общему принципу, b должна идти перед k. Однако b зависит от k. Поэтому мы отклоняем T2 с соответствующим сообщением об ошибке.

В ассоциированных типах мы упорядочиваем переменные типа так, как если бы семейство типов было объявлением верхнего уровня, игнорируя видимость связывателей переменных типа класса. Вот пример:

class C (a :: k) b where
  type F (c :: j) (d :: Proxy m) a b

Мы выводим следующие виды:

C :: forall {k1 :: Type} (k :: Type). k -> k1 -> Constraint
F :: forall {k1 :: Type} {k2 :: Type} {k3 :: Type} j (m :: k1).
     j -> Proxy m -> k2 -> k3 -> Type

Обратите внимание, что вид a задан в виде C, но выведен в виде F.

Описанный здесь «общий принцип» должен сделать поведение более предсказуемым для пользователей. Расширить GHC, чтобы ослабить это правило, было бы нетрудно. Если вы хотите предложить такое изменение, рассмотрите возможность написать предложение.

6.4.14.7. Полные сигнатуры видов, заданные пользователем, и полиморфная рекурсия

CUSKs

Начиная с:

8.10.1

Статус:

Включено в Haskell98, Haskell2010

Внимание! Это устаревшая возможность; современная замена описана в разделе StandaloneKindSignatures.

Как и при выводе типов, для рекурсивных типов при выводе видов возможна только мономорфная рекурсия. Рассмотрим следующий (искусственный) пример:

data T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind  T :: (Type -> Type) -> Type -> Type

Рекурсивное использование T вынуждает второй аргумент иметь вид Type. Однако, как и при выводе типов, полиморфной рекурсии можно добиться, задав для T полную сигнатуру вида, заданную пользователем (или CUSK). CUSK присутствует, если виды всех аргументов и результат известны без необходимости вывода. Например:

data T (m :: k -> Type) :: k -> Type where
  MkT :: m a -> T Maybe (m a) -> T m a

Полная сигнатура вида, заданная пользователем, указывает полиморфный вид для T, и эта сигнатура используется во всех вызовах T, включая рекурсивные. В частности, рекурсивное использование T имеет вид Type.

Что именно считается «полной сигнатурой вида, заданной пользователем» для конструктора типа? К таким формам относятся:

• Для типа данных каждый параметр типа должен иметь аннотацию вида. В объявлении в стиле GADT также может присутствовать сигнатура вида (с :: верхнего уровня в заголовке), но наличие или отсутствие этой аннотации не влияет на то, считается ли объявление полным.

  data T1 :: (k -> Type) -> k -> Type       where ...
  -- Yes;  T1 :: forall k. (k->Type) -> k -> Type
  
  data T2 (a :: k -> Type) :: k -> Type     where ...
  -- Yes;  T2 :: forall k. (k->Type) -> k -> Type
  
  data T3 (a :: k -> Type) (b :: k) :: Type where ...
  -- Yes;  T3 :: forall k. (k->Type) -> k -> Type
  
  data T4 (a :: k -> Type) (b :: k)      where ...
  -- Yes;  T4 :: forall k. (k->Type) -> k -> Type
  
  data T5 a (b :: k) :: Type             where ...
  -- No;  kind is inferred
  
  data T6 a b                         where ...
  -- No;  kind is inferred
  

• Для типа данных с :: верхнего уровня все переменные вида, введённые после ::, должны быть явно квантифицированы.

  data T1 :: k -> Type            -- No CUSK: `k` is not explicitly quantified
  data T2 :: forall k. k -> Type  -- CUSK: `k` is bound explicitly
  data T3 :: forall (k :: Type). k -> Type   -- still a CUSK
  

• Для newtype действуют те же правила, что и для типа данных, если не включено UnliftedNewtypes. При включённом UnliftedNewtypes конструктор типа имеет CUSK только при наличии сигнатуры вида. Как и для типа данных с :: верхнего уровня, все переменные вида, введённые после ::, должны быть явно квантифицированы

  {-# LANGUAGE UnliftedNewtypes #-}
  newtype N1 where                 -- No; missing kind signature
  newtype N2 :: TYPE IntRep where  -- Yes; kind signature present
  newtype N3 (a :: Type) where     -- No; missing kind signature
  newtype N4 :: k -> Type where    -- No; `k` is not explicitly quantified
  newtype N5 :: forall (k :: Type). k -> Type where -- Yes; good signature
  

• Для класса каждый параметр типа должен иметь аннотацию вида.

• Для синонима типа аннотациями видов должны быть снабжены все параметры типа и результирующий тип:

  type S1 (a :: k) = (a :: k)    -- Yes   S1 :: forall k. k -> k
  type S2 (a :: k) = a           -- No    kind is inferred
  type S3 (a :: k) = Proxy a     -- No    kind is inferred
  

  Обратите внимание: хотя в S2 и S3 вид правой части достаточно очевиден, такие объявления всё равно не считаются имеющими полную сигнатуру — вывод не может выполняться до обнаружения сигнатуры.

• Несвязанное объявление открытого семейства типов или данных всегда имеет CUSK; для параметров типа без аннотаций по умолчанию используется вид Type:

  data family D1 a                  -- D1 :: Type -> Type
  data family D2 (a :: k)           -- D2 :: forall k. k -> Type
  data family D3 (a :: k) :: Type   -- D3 :: forall k. k -> Type
  type family S1 a :: k -> Type     -- S1 :: forall k. Type -> k -> Type
  

• Ассоциированное объявление семейства типов или данных имеет CUSK тогда и только тогда, когда CUSK имеет окружающий его класс.

  class C a where                -- no CUSK
    type AT a b                  -- no CUSK, b is defaulted
  
  class D (a :: k) where         -- yes CUSK
    type AT2 a b                 -- yes CUSK, b is defaulted
  

• Замкнутое семейство типов имеет полную сигнатуру, если для всех его параметров типа заданы аннотации и указаны возвращаемый вид (с :: верхнего уровня).

Можно написать тип данных, который синтаксически имеет CUSK (согласно правилам выше), но фактически требует вывода. Рассмотрим весьма искусственный пример:

data Proxy a           -- Proxy :: forall k. k -> Type
data X (a :: Proxy k)

Согласно приведённым выше правилам, X имеет CUSK. Однако вид k не определён. Поэтому он квантифицируется, и X получает вид forall k1 (k :: k1). Proxy k -> Type.

Обнаружение CUSK включается флагом CUSKs. По умолчанию он выключен в GHC2021 и включён в Haskell98 и Haskell2010. Это расширение планируется объявить устаревшим и заменить на StandaloneKindSignatures.

6.4.14.8. Автономные сигнатуры видов и полиморфная рекурсия

StandaloneKindSignatures

Подразумевает:

NoCUSKs

Начиная с:

8.10.1

Статус:

Включено в GHC2024, GHC2021

Как и при выводе типов, для рекурсивных типов при выводе видов возможна только мономорфная рекурсия. Рассмотрим следующий (искусственный) пример:

data T m a = MkT (m a) (T Maybe (m a))
-- GHC infers kind  T :: (Type -> Type) -> Type -> Type

Рекурсивное использование T вынуждает второй аргумент иметь вид Type. Однако, как и при выводе типов, полиморфной рекурсии можно добиться, задав для T автономную сигнатуру вида:

type T :: (k -> Type) -> k -> Type
data T m a = MkT (m a) (T Maybe (m a))

Автономная сигнатура вида задаёт полиморфный вид для T, и эта сигнатура используется во всех вызовах T, включая рекурсивные. В частности, рекурсивное использование T имеет вид Type.

Автономная сигнатура вида определяет вид конструктора типа, но не его арность. Это особенно важно для семейств типов и синонимов типов, поскольку их нельзя применить частично. Подробнее об арности см. в разделе Объявления семейств типов.

Арность можно указать с помощью явных связывателей и встроенных аннотаций видов:

-- arity F0 = 0
type F0 :: forall k. k -> Type
type family F0 :: forall k. k -> Type

-- arity F1 = 1
type F1 :: forall k. k -> Type
type family F1 :: k -> Type

-- arity F2 = 2
type F2 :: forall k. k -> Type
type family F2 a :: Type

Если встроенная аннотация вида отсутствует, выведенная арность включает все явно связанные параметры и все непосредственно следующие за ними невидимые параметры:

-- arity FD1 = 1
type FD1 :: forall k. k -> Type
type FD1

-- arity FD2 = 2
type FD2 :: forall k. k -> Type
type FD2 a

Обратите внимание, что F0, F1, F2, FD1 и FD2 имеют идентичные автономные сигнатуры видов. Арность выводится из заголовка семейства типов.

Переменные вида, связанные внешним forall в автономной сигнатуре вида, ограничены областью видимости только вида в этой сигнатуре. В отличие от сигнатур типов на уровне термов (см. Сигнатуры типов в объявлениях), внешние переменные вида не ограничивают областью видимости соответствующее объявление. Например, дано следующее объявление класса:

class C (a :: k) where
  m :: Proxy k -> Proxy a -> String

Следующее определение C не будет эквивалентным:

type C :: forall k. k -> Constraint
class C a where
  m :: Proxy k -> Proxy a -> String

Поскольку k из автономной сигнатуры вида не ограничивает областью видимости определение C, k в сигнатуре типа m больше не является видом a, а представляет собой совершенно другой вид. Это равносильно следующему определению:

type C :: forall k. k -> Constraint
class C (a :: kindOfA) where
  m :: forall k. Proxy k -> Proxy (a :: kindOfA) -> String

Чтобы избежать этой проблемы, определение C должно содержать встроенную аннотацию вида, например:

type C :: forall k. k -> Constraint
class C (a :: k) where
  m :: Proxy k -> Proxy a -> String

6.4.14.9. Автономные сигнатуры видов и заголовки объявлений

Если присутствует автономная сигнатура вида, GHC требует, чтобы в объявлениях data были связаны все параметры. Например:

type Prox1 :: k -> Type
data Prox1 a = MkProx1
  -- OK.

type Prox2 :: k -> Type
data Prox2 = MkProx2
  -- Error:
  --   • Expected a type, but found something with kind ‘k -> Type’
  --   • In the data type declaration for ‘Prox2’

Объявления data в стиле GADT могут либо связывать свои параметры, либо использовать встроенную сигнатуру в дополнение к автономной сигнатуре вида:

type GProx1 :: k -> Type
data GProx1 a where MkGProx1 :: GProx1 a
  -- OK.

type GProx2 :: k -> Type
data GProx2 where MkGProx2 :: GProx2 a
  -- Error:
  --   • Expected a type, but found something with kind ‘k -> Type’
  --   • In the data type declaration for ‘GProx2’

type GProx3 :: k -> Type
data GProx3 :: k -> Type where MkGProx3 :: GProx3 a
  -- OK.

type GProx4 :: k1 -> Type
data GProx4 :: k2 -> Type where MkGProx4 :: GProx4 a
  -- OK.

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

type GProx5 :: k -> Type
data GProx5 :: w where MkGProx5 :: GProx5 a
  -- Error:
  --   • Couldn't match expected kind ‘w’ with actual kind ‘k -> Type’
  --   • In the data type declaration for ‘GProx5’

Классы подчиняются тем же правилам:

type C1 :: Type -> Constraint
class C1 a
  -- OK.

type C2 :: Type -> Constraint
class C2
  -- Error:
  --   • Couldn't match expected kind ‘Constraint’
  --                 with actual kind ‘Type -> Constraint’
  --   • In the class declaration for ‘C2’

Для семейств типов количество параметров в сигнатуре вида имеет дополнительное значение: оно задаёт арность семейства типов, то есть количество аргументов, которое требуется семейству типов для редукции. Все экземпляры семейства типов должны предоставлять такое же количество аргументов. Например:

type F1 :: Type -> Type
type family F1 where
  F1 = Maybe
  -- OK.

type F2 :: Type -> Type
type family F2 where
  F2 () = Bool
  F2 a  = Maybe a
  -- Error:
  --   • Number of parameters must match family declaration; expected 0
  --   • In the type family declaration for `F2'

type F3 :: Type -> Type
type family F3 a where
  F3 () = Bool
  F3 a  = Maybe a
  -- OK.

Семейства данных — более сложный случай. На их заголовки это правило не распространяется, но на их экземпляры — распространяется:

type T :: k -> Type
data family T
  -- OK.

data instance T Int = MkT1
  -- OK.

data instance T = MkT3
  -- Error:
  --   • Expecting one more argument to ‘T’
  --     Expected a type, but ‘T’ has kind ‘k0 -> Type’
  --   • In the data instance declaration for ‘T’

Это также относится к экземплярам данных в стиле GADT:

data instance T (a :: Nat) where MkN4 :: T 4
                                 MKN9 :: T 9
  -- OK.

data instance T :: Symbol -> Type where MkSN :: T "Neptune"
                                        MkSJ :: T "Jupiter"
  -- OK.

data instance T where MkT4 :: T x
  -- Error:
  --   • Expecting one more argument to ‘T’
  --     Expected a type, but ‘T’ has kind ‘k0 -> Type’
  --   • In the data instance declaration for ‘T’

6.4.14.10. Вывод вида в объявлениях типов данных

Рассмотрим объявление

data T1 f a = MkT1 (f a)
data T2 f a where
  MkT2 :: f a -> T f a

В обоих случаях GHC анализирует объявления конструкторов данных, чтобы задать ограничения на вид T, получая

T1, T2 :: forall k. (k -> Type) -> k -> Type

Рассмотрим тип

type G :: forall k. k -> Type
data G (a :: k) where
  GInt    :: G Int
  GMaybe  :: G Maybe

Этот тип данных G похож на GADT и по виду, и по типу. Предположим, что у нас есть g :: G a, где a :: k. Сопоставление с образцом, позволяющее установить, что g на самом деле является GMaybe, сообщает нам и о том, что k ~ (Type -> Type), и о том, что a ~ Maybe. Для определения G требуется включить PolyKinds, но для сопоставления с образцом G не требуется никаких расширений, кроме GADTs. Такая возможность — простое расширение обычных GADT и следствие того, что виды и типы — одно и то же.

Обратите внимание, что тип данных G в своём теле используется с разными видами, поэтому индексированные по видам GADT используют форму полиморфной рекурсии. Следовательно, эта возможность доступна только при наличии полной сигнатуры вида, заданной пользователем (CUSK) для типа данных (Полные сигнатуры видов, заданные пользователем, и полиморфная рекурсия), или автономной сигнатуры вида (Автономные сигнатуры видов и полиморфная рекурсия); для G используются обе. Чтобы явно увидеть индексацию по видам, включите -fprint-explicit-kinds и запросите информацию о G с помощью команды GHCi :info:

> :set -fprint-explicit-kinds
> :info G
type role G nominal nominal
type G :: forall k. k -> Type
data G @k a where
  GInt   :: G @Type Int
  GMaybe :: G @(Type -> Type) Maybe

как видно, оба конструктора обладают свойствами GADT.

6.4.14.11. Вывод вида для объявлений экземпляров data/newtype

Рассмотрим следующие объявления

data family T :: forall k. (k -> Type) -> k -> Type

data instance T p q where
   MkT :: forall r. r Int -> T r Int

Здесь T имеет невидимый аргумент вида; возможно, в экземпляре он инстанцируется в Type, например:

data instance T @Type (p :: Type -> Type) (q :: Type) where
   MkT :: forall r. r Int -> T r Int

Или, возможно, мы подразумевали специализацию в конструкторе данных GADT, например:

data instance T @k (p :: k -> Type) (q :: k) where
   MkT :: forall r. r Int -> T @Type r Int

С несколькими конструкторами всё становится сложнее. В общем случае нет принципиального способа определить, какая специализация типа относится к экземпляру данных, а какая — к отдельным конструкторам данных GADT.

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

6.4.14.12. Вывод вида в объявлениях экземпляров классов

Рассмотрим следующий пример класса с полиморфным видом и его экземпляра:

class C a where
  type F a

instance C b where
  type F b = b -> b

В объявлении класса ничто не ограничивает вид типа a, поэтому он становится полиморфной по видам переменной типа (a :: k). Однако правая часть экземпляра ассоциированного типа b -> b в объявлении экземпляра указывает, что b должен иметь вид Type. Теоретически GHC мог бы передать эту информацию обратно в заголовок экземпляра и ограничить действие объявления экземпляра типами вида Type, а не типами любого вида. Однако GHC этого не делает.

Кратко: GHC не передаёт информацию о видах из членов объявления экземпляра класса в заголовок этого объявления.

Отсутствие такого вывода видов — лишь инженерная проблема GHC, но его реализация потребовала бы существенных изменений в инфраструктуре вывода, и неясно, оправдали бы себя затраты. Если вы хотите ограничить вид b в приведённом выше экземпляре, просто используйте сигнатуру вида в заголовке экземпляра.

6.4.14.13. Вывод вида в синонимах типов и экземплярах семейств типов

Рассмотрим правила области видимости для синонимов типов и экземпляров семейств типов, например:

type          TS a (b :: k) = <rhs>
type instance TF a (b :: k) = <rhs>

Основной принцип заключается в том, что все переменные, упомянутые в правой части <rhs>, должны быть связаны в левой части:

type TS a (b :: k) = (k, a, Proxy b)    -- accepted
type TS a (b :: k) = (k, a, Proxy b, z) -- rejected: z not in scope

Но есть одно исключение: свободные переменные, упомянутые во внешней аннотации вида в правой части, квантифицируются неявно. Поэтому в следующем примере переменные a, b и k находятся в области видимости в правой части S:

type S a b = <rhs> :: k -> k

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

S :: forall k. Type -> Type -> k -> k

В этом случае мы не можем просто связать k в левой части, поскольку k станет видимым параметром:

type S k a b = <rhs> :: k -> k
S :: forall k -> Type -> Type -> k -> k

Обратите внимание, что при определении переменных для неявной квантификации мы рассматриваем только внешнюю аннотацию вида. В качестве контрпримера рассмотрим M1:

type M1 = Just (Nothing :: Maybe k)    -- rejected: k not in scope

Здесь аннотация вида находится внутри Just, и внешней аннотации вида нет. Этот пример можно исправить, добавив внешнюю аннотацию вида:

type M2 = Just (Nothing :: Maybe k) :: Maybe (Maybe k)

Здесь k вводится в область видимости посредством :: Maybe (Maybe k).

Аннотация вида считается внешней независимо от наличия избыточных скобок:

type P =    Nothing :: Maybe a    -- accepted
type P = (((Nothing :: Maybe a))) -- accepted

К закрытым экземплярам семейств типов применяются те же правила:

type family F where
  F = Nothing :: Maybe k            -- accepted

type family F where
  F = Just (Nothing :: Maybe k)     -- rejected: k not in scope

type family F where
  F = Just (Nothing :: Maybe k) :: Maybe (Maybe k)  -- accepted

type family F :: Maybe (Maybe k) where
  F = Just (Nothing :: Maybe k)     -- rejected: k not in scope

type F :: forall k. Maybe (Maybe k)
type family F @k where
  F @k = Just (Nothing :: Maybe k)  -- accepted

-- CUSKs version (Legacy)
type family F :: Maybe (Maybe k) where
  F @k = Just (Nothing :: Maybe k)  -- accepted

Переменные вида также могут квантифицироваться в видимых позициях. Рассмотрим следующие два примера:

data ProxyKInvis (a :: k)
data ProxyKVis k (a :: k)

В первом примере переменная вида k является невидимым аргументом ProxyKInvis. Иными словами, пользователю не нужно явно инстанцировать k, поскольку вывод вида автоматически определяет, каким должно быть k. Например, в ProxyKInvis True переменная k выводится как Bool. Это отражено в виде ProxyKInvis:

ProxyKInvis :: forall k. k -> Type

Во втором примере k является видимым аргументом ProxyKVis. То есть k — это аргумент, который пользователи должны явно указывать при применении ProxyKVis. Например, ProxyKVis Bool True — корректный тип.

Каков вид ProxyKVis? Можно было бы сказать forall k. Type -> k -> Type, но это не совсем верно, поскольку такое утверждение допускало бы некорректные выражения, например ProxyKVis Bool Int, которые следует отклонить, так как Int не имеет вида Bool. Ключевое наблюдение заключается в том, что вид второго аргумента зависит от первого. GHC обозначает эту зависимость в синтаксисе, который используется для записи вида ProxyKVis:

ProxyKVis :: forall k -> k -> Type

Этот вид похож на вид ProxyKInvis, но есть важное различие: за переменными типа, квантифицируемыми с помощью forall, следует стрелка (->), а не точка (.). Это видимый зависимый квантор. Он видимый, поскольку пользователь должен явно передать тип для k, и зависимый, поскольку k появляется далее в виде ProxyKVis. В качестве соответствующего понятия связыватель k в forall k. k -> Type можно считать невидимым зависимым квантором.

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

ProxyKVis :: forall (k :: Type) -> k -> Type

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

6.4.14.14. Вывод вида в закрытых семействах типов

Хотя считается, что для всех открытых семейств типов полная сигнатура вида предоставляется пользователем (Полные сигнатуры вида, предоставляемые пользователем, и полиморфная рекурсия), для закрытых семейств типов это требование можно ослабить, поскольку у нас есть уравнения, на основе которых можно выводить виды. GHC выведет виды аргументов и результирующих типов закрытого семейства типов.

GHC поддерживает семейства типов, индексированные видом, в которых семейство сопоставляется как с видом, так и с типом. GHC не будет выводить такое поведение без полной сигнатуры вида, предоставленной пользователем, или отдельной сигнатуры вида (см. Отдельные сигнатуры вида и полиморфная рекурсия), поскольку в некоторых случаях это привело бы к выводу не главных типов. Действительно, индексирование по виду можно рассматривать как форму полиморфной рекурсии, при которой тип в собственном определении используется с видом, отличным от наиболее общего для него.

Например:

type family F1 a where
  F1 True  = False
  F1 False = True
  F1 x     = x
-- F1 fails to compile: kind-indexing is not inferred

type family F2 (a :: k) where
  F2 True  = False
  F2 False = True
  F2 x     = x
-- F2 fails to compile: no complete signature

type F3 :: k -> k
type family F3 a where
  F3 True  = False
  F3 False = True
  F3 x     = x

-- CUSKs version (legacy)
type family F4 (a :: k) :: k where
  F4 True  = False
  F4 False = True
  F4 x     = x
-- OK

6.4.14.15. Виды высших рангов

В сочетании с RankNTypes GHC поддерживает виды высших рангов. Вот пример:

-- Heterogeneous propositional equality
data (a :: k1) :~~: (b :: k2) where
  HRefl :: a :~~: a

class HTestEquality (t :: forall k. k -> Type) where
  hTestEquality :: forall k1 k2 (a :: k1) (b :: k2). t a -> t b -> Maybe (a :~~: b)

Обратите внимание, что hTestEquality принимает два аргумента, причём переменная типа t применяется к типам с разными видами. Следовательно, эта переменная типа должна быть поливидовой. Поэтому вид HTestEquality (класса) равен (forall k. k -> Type) -> Constraint — это вид высшего ранга.

Виды высших рангов существенно отличаются от типов высших рангов тем, что forall в видах нельзя перемещать. Лучше всего это показать на примере. Предположим, что мы хотим создать экземпляр HTestEquality для (:~~:).

instance HTestEquality ((:~~:) a) where
  hTestEquality HRefl HRefl = Just HRefl

С приведённым выше объявлением (:~~:) получает вид forall k1 k2. k1 -> k2 -> Type. Таким образом, тип (:~~:) a имеет вид k2 -> Type для некоторого k2. После этого GHC не может повторно обобщить этот вид, чтобы получить требуемый forall k2. k2 -> Type. Поэтому экземпляр отклоняется как имеющий некорректный вид.

Чтобы разрешить такой экземпляр, необходимо определить (:~~:) следующим образом:

data (:~~:) :: forall k1. k1 -> forall k2. k2 -> Type where
  HRefl :: a :~~: a

В этом переопределении мы задаём явный вид для (:~~:), откладывая выбор k2 до момента, когда будет задан первый аргумент (a). При таком объявлении (:~~:) экземпляр для HTestEquality принимается.

6.4.14.16. Вид Type

StarIsType

Начиная с:

8.6.1

Статус:

Включено в GHC2024, GHC2021, Haskell2010, Haskell98

Рассматривать неквалифицированные вхождения оператора типа * как нульарные и выполнять их десахаризацию в Data.Kind.Type.

Вид Type (импортированный из Data.Kind) классифицирует обычные типы. При включённом расширении StarIsType (сейчас оно включено по умолчанию) * десахаризуется в Type, однако использовать этот устаревший синтаксис не рекомендуется из-за конфликтов с TypeOperators. То же относится к ★ — Unicode-варианту *.

6.4.14.17. Вывод зависимостей в объявлениях типов данных

Если переменная типа a в объявлении типа данных, класса или семейства типов зависит от другой такой переменной k в том же объявлении, должны выполняться два условия:

• a должна идти после k в объявлении, и
• k должна явно присутствовать в виде некоторой переменной типа в этом объявлении.

Первый пункт означает, что зависимость должна быть корректной с точки зрения области видимости. Второй пункт относится к способности GHC выводить зависимость. Выводить её сложно, поэтому в настоящее время GHC требует указывать зависимость явно: k должна присутствовать в виде переменной типа, чтобы GHC мог однозначно определить, что подразумевается зависимость. Например:

data Proxy k (a :: k)            -- OK: dependency is "obvious"
data Proxy2 k a = P (Proxy k a)  -- ERROR: dependency is unclear

Во втором объявлении GHC не может сразу понять, что k должна быть зависимой переменной, поэтому объявление отклоняется.

Возможно, в будущем это ограничение будет ослаблено, но на момент написания документа неясно, связаны ли трудности в этом случае с теорией (вывод такой зависимости означал бы, что наша система типов не имеет главных типов) или только с практической стороной (вывод такой зависимости сложен с учётом реализации GHC). Поэтому GHC выбирает простой путь и просит пользователя немного помочь.

6.4.14.18. Вывод зависимостей в записанных пользователем forall

Программист может использовать forall в типе, чтобы ввести новые квантифицированные переменные типа. Эти переменные могут зависеть друг от друга, даже если они находятся в одном forall. Однако GHC требует, чтобы зависимость можно было вывести из тела forall. Вот несколько примеров:

data Proxy k (a :: k) = MkProxy   -- just to use below

f :: forall k a. Proxy k a        -- This is just fine. We see that (a :: k).
f = undefined

g :: Proxy k a -> ()              -- This is to use below.
g = undefined

data Sing a
h :: forall k a. Sing k -> Sing a -> ()  -- No obvious relationship between k and a
h _ _ = g (MkProxy :: Proxy k a)  -- This fails. We didn't know that a should have kind k.

Обратите внимание, что в последнем примере из тела forall (то есть Sing k -> Sing a -> ()) невозможно понять, что a зависит от k. Поэтому GHC отклоняет программу.

6.4.14.19. Подстановка вида по умолчанию без PolyKinds

Без расширения PolyKinds GHC отказывается обобщать переменные вида. Поэтому, когда это возможно, он подставляет вместо переменных вида Type; если это невозможно, выдаётся ошибка.

Вот пример такого поведения:

{-# LANGUAGE PolyKinds #-}
import Data.Kind (Type)
data Proxy a = P   -- inferred kind: Proxy :: k -> Type
data Compose f g x = MkCompose (f (g x))
  -- inferred kind: Compose :: (b -> Type) -> (a -> b) -> a -> Type

-- separate module having imported the first
{-# LANGUAGE NoPolyKinds, DataKinds #-}
z = Proxy :: Proxy MkCompose

В последней строке мы используем повышенный конструктор MkCompose, имеющий вид

forall (a :: Type) (b :: Type) (f :: b -> Type) (g :: a -> b) (x :: a).
  f (g x) -> Compose f g x

Теперь нам нужно вывести тип для z. Чтобы сделать это без обобщения переменных вида, необходимо подставить значения по умолчанию для переменных вида в MkCompose. Мы без труда можем подставить Type вместо a и b, но при такой подстановке f и g имели бы некорректный вид. Поэтому определение z приводит к ошибке.

6.4.14.20. Форматирование вывода при полиморфизме по виду

При полиморфизме по виду за кулисами происходит довольно много всего, что может быть незаметно программисту на Haskell. В GHC есть несколько флагов, управляющих тем, как типы отображаются в сообщениях об ошибках и в приглашении GHCi. Подробнее см. обсуждение параметров форматирования вывода типов. Если вы используете полиморфизм по виду и не понимаете, почему GHC отклоняет (или принимает) вашу программу, рекомендуем включить эти флаги, особенно -fprint-explicit-kinds.

6.4.14.21. Возвращаемые виды типов данных

С расширением KindSignatures можно задавать вид типа данных, записанного в синтаксисе GADT (см. GADTSyntax). Например:

data T :: Type -> Type where ...

Для этих возвращаемых видов действует ряд ограничений. В приведённом ниже тексте рассматриваются UnliftedNewtypes и семейства данных (включаемые расширением TypeFamilies). Кроме того, предполагается знакомство с полиморфизмом представления.

1. Объявления data и data instance должны иметь возвращаемые виды, заканчивающиеся на TYPE LiftedRep. (Напомним, что Type — это просто синоним TYPE LiftedRep.) Под «заканчивающимися на» подразумевается вид, остающийся после удаления всех аргументов (введённых посредством forall или ->) и раскрытия синонимов типов. Обратите внимание, что при этой проверке семейства типов не раскрываются.

2. Если включено расширение UnliftedNewtypes, объявления newtype и newtype instance должны иметь возвращаемые виды, заканчивающиеся на TYPE rep для некоторого rep. rep может содержать семейства типов, но TYPE должно быть очевидно без раскрытия семейств типов. Раскрытие синонимов типов допустимо.

   Если расширение UnliftedNewtypes не включено, на объявления newtype и newtype instance накладываются те же ограничения, что и на объявления data.

3. Экземпляр data или newtype фактически может иметь два возвращаемых вида. Первый — это вид, полученный применением семейства данных к образцам, указанным в объявлении экземпляра. Второй задаётся аннотацией вида. Оба возвращаемых вида должны удовлетворять приведённым выше ограничениям.

Примеры:

data T1 :: Type             -- good: Type expands to TYPE LiftedRep
data T2 :: TYPE LiftedRep   -- good
data T3 :: forall k. k -> Type -> Type  -- good: arguments are dropped

type LR = LiftedRep
data T3 :: TYPE LR          -- good: we look through type synonyms

type family F a where
  F Int = LiftedRep

data T4 :: TYPE (F Int)     -- bad: we do not look through type families

type family G a where
  G Int = Type

data T5 :: G Int            -- bad: we do not look through type families

-- assume -XUnliftedNewtypes
newtype T6 :: Type where ...             -- good
newtype T7 :: TYPE (F Int) where ...     -- good
newtype T8 :: G Int where ...            -- bad

data family DF a :: Type
data instance DF Int :: Type             -- good
data instance DF Bool :: TYPE LiftedRep  -- good
data instance DF Char :: G Int           -- bad

data family DF2 k :: k                   -- good
data family DF2 Type                     -- good
data family DF2 Bool                     -- bad
data family DF2 (G Int)                  -- bad for 2 reasons:
                                         --  a type family can't be in a pattern, and
                                         --  the kind fails the restrictions here