6.4.13. Полиморфизм видов

6.4.13.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 выводит вид forall k. (k -> Type) -> k -> Type для App, который является его наиболее общим видом.

Таким образом, основное преимущество полиморфизма видов заключается в том, что теперь мы можем вывести эти наиболее общие виды и использовать 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.13.2. Обзор типа в типе

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

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

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

6.4.13.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 выводит наиболее полиморфный вид, совместимый с правой частью. Примеры: обычные объявления типов данных и GADTs, объявления классов. В случае объявления класса роль «правой части» играют сигнатуры методов класса.
• Если правой части нет, 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.13.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.13.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.13.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.13.7. Полные пользовательские подписи вида и полиморфная рекурсия

CUSKs

Since:

8.10.1

Status:

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

ПРИМЕЧАНИЕ! Это устаревшая функция, см. StandaloneKindSignatures для замены.

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

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

Рекурсивное использование T заставило второй аргумент иметь вид Type. Однако, так же, как и в выводе типов, вы можете добиться полиморфной рекурсии, предоставив полную пользовательскую подпись вида (или CUSK) для T. 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.13.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.13.9. Автономные сигнатуры видов и заголовки объявлений

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

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’

Объявления данных в стиле 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.13.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. То, что это работает, на самом деле является простым расширением обычных GADTs и следствием того, что виды и типы одинаковы.

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

> :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.13.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.13.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.13.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.13.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.13.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.13.16. Тип вида Type

StarIsType

Since:

8.6.1

Status:

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

Обрабатывать неквалифицированные использования оператора типа * как нульарные и развёртывать до Data.Kind.Type.

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

6.4.13.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.13.18. Вывод зависимости в пользовательских foralls

Программист может использовать 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.

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

6.4.13.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. Мы можем легко задать значения по умолчанию a и b как Type, но f и g будут иметь неправильные виды, если им задать значения по умолчанию. Таким образом, определение для z является ошибкой.

6.4.13.20. Вывод в формате для отображения при наличии полиморфизма видов

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

6.4.13.21. Виды возврата для типов данных

С KindSignatures, мы можем задать вид для типа данных, написанного в синтаксисе GADTs (см. 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