6.4.10. Семейства типов

6.4.10.1.1. Объявления семейств данных

Индексированные семейства данных вводятся сигнатурой, например

data family GMap k :: Type -> Type

Специальный family отличает семейство от стандартного объявления data. Аннотация результирующего рода необязательна и, как обычно, по умолчанию равна Type, если её не указать. Например:

data family Array e

При необходимости именованным аргументам также можно явно указать сигнатуры рода. Как и в случае с объявлениями GADT, именованные аргументы полностью необязательны, поэтому вместо этого можно объявить Array следующим образом:

data family Array :: Type -> Type

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

• Вида TYPE r для некоторого r (см. полиморфизм представления). Например:

  data family DF1 :: TYPE IntRep
  data family DF2 (r :: RuntimeRep)  :: TYPE r
  data family DF3 :: Type -> TYPE WordRep
  

• Просто переменной рода (при включённом PolyKinds). Например:

  data family DF4 :: k
  data family DF5 (a :: k) :: k
  data family DF6 :: (k -> Type) -> k
  

Однако роды экземпляров данных должны оканчиваться на Type. Это ограничение немного ослабляется при включённом расширении UnliftedNewtypes, поскольку оно позволяет роду newtype instance оканчиваться на TYPE r для некоторого r.

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

Объявления экземпляров семейств данных и newtype очень похожи на стандартные объявления data и newtype. Различий всего два: за ключевым словом data или newtype следует instance, а некоторые или все аргументы типа могут быть не переменными, но не могут содержать типы forall или семейства синонимов типов. Однако семейства данных, как правило, разрешены в параметрах типа, а синонимы типов допустимы, если они применены ко всем аргументам и раскрываются в допустимый тип — точно так же, как это требуется для вхождений синонимов типов в параметрах экземпляров классов. Например, экземпляр Either для GMap выглядит так:

data instance GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)

В этом примере объявление содержит только один вариант. В общем случае их может быть любое количество.

Если включено расширение ExplicitForAll, переменные типов и родов, используемые в левой части, можно связать явно. Например:

data instance forall a (b :: Proxy a). F (Proxy b) = FProxy Bool

Если присутствует явный forall, все упомянутые переменные типов и родов, которых ещё нет в области видимости, должны быть связаны в forall:

data instance forall   (a :: k). F a = FOtherwise  -- rejected: k not in scope
data instance forall k (a :: k). F a = FOtherwise  -- accepted

Если включён флаг -Wunused-type-patterns, компилятор сообщает о переменных типов, упомянутых в шаблонах левой части, но не используемых в правой. Переменные, встречающиеся в левой части несколько раз, также считаются использованными. Чтобы подавить предупреждения, неиспользуемые переменные следует заменить или предварить символами подчёркивания. В остальном переменные типов, начинающиеся с подчёркивания (_x), рассматриваются как обычные переменные типов.

Это похоже на подстановочные знаки, которые можно использовать в частичных сигнатурах типов. Однако есть и некоторые отличия. Сообщения об ошибках с выводом типов не генерируются, а расширение PartialTypeSignatures не оказывает никакого влияния.

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

Объявления экземпляров data и newtype разрешены только при наличии в области видимости соответствующего объявления семейства — так же, как для объявления экземпляра класса требуется, чтобы объявление класса было видимым. Кроме того, каждое объявление экземпляра должно соответствовать роду, заданному объявлением семейства. Это означает, что число параметров объявления экземпляра должно соответствовать арности, определяемой родом семейства.

Объявление экземпляра семейства данных может использовать все выразительные возможности обычных объявлений data или newtype:

• Хотя семейство данных вводится ключевым словом «data», для экземпляра семейства данных можно использовать как data, так и newtype. Например:

  data family T a
  data    instance T Int  = T1 Int | T2 Bool
  newtype instance T Char = TC Bool
  

• В data instance для конструкторов данных можно использовать синтаксис GADT и, в частности, определить GADT. Например:

  data family G a b
  data instance G [a] b where
     G1 :: c -> G [Int] b
     G2 :: G [a] Bool
  

• В объявлении data instance или newtype instance можно использовать предложение deriving.

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

data family T a
data instance T Int  = A
data instance T Char = B
foo :: T a -> Int
foo A = 1
foo B = 2

Вместо этого необходимо объявить foo как операцию класса, например так:

class Foo a where
  foo :: T a -> Int
instance Foo Int where
  foo A = 1
instance Foo Char where
  foo B = 2

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

6.4.10.1.3. Перекрытие экземпляров данных

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

6.4.10.2.1. Объявления семейств типов

Открытые индексированные семейства типов вводятся сигнатурой, например

type family Elem c :: Type

Специальный family отличает семейство от стандартного объявления типа. Аннотация результирующего рода необязательна и, как обычно, по умолчанию равна Type, если её не указать. Например:

type family Elem c

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

type family F a b :: Type -> Type
  -- F's arity is 2,
  -- although its overall kind is Type -> Type -> Type -> Type

Для этого объявления ниже приведены примеры корректных и некорректных типов:

F Char [Int]       -- OK!  Kind: Type -> Type
F Char [Int] Bool  -- OK!  Kind: Type
F IO Bool          -- WRONG: kind mismatch in the first argument
F Bool             -- WRONG: unsaturated application

Аннотация результирующего рода необязательна и, если она не указана, по умолчанию равна Type (как и роды аргументов). Семейства типов с полиморфными родами можно объявлять, используя параметр в аннотации рода:

type family F a :: k

В этом случае параметр рода k фактически является неявным параметром семейства типов.

При определении арность задаёт, какие входные данные можно сопоставлять с образцом:

data PT (a :: Type)

type family F1 :: k -> Type
type instance F1 = PT
  -- OK, 'k' can be matched on.

type family F0 :: forall k. k -> Type
type instance F0 = PT
  -- Error:
  --   • Expected kind ‘forall k. k -> Type’,
  --       but ‘PT’ has kind ‘Type -> Type’
  --   • In the type ‘PT’
  --     In the type instance declaration for ‘F0’

Рода обоих типов F1 и F0 равны forall k. k -> Type, но их арности различаются.

В местах использования арность определяет, можно ли использовать определение в сценарии с полиморфизмом более высокого ранга:

type HRK (f :: forall k. k -> Type) = (f Int, f Maybe, f True)

type H1 = HRK F0  -- OK
type H2 = HRK F1
  -- Error:
  --   • Expected kind ‘forall k. k -> Type’,
  --       but ‘F1’ has kind ‘k0 -> Type’
  --   • In the first argument of ‘HRK’, namely ‘F1’
  --     In the type ‘HRK F1’
  --     In the type declaration for ‘H2’

Это следствие требования, согласно которому все применения семейства типов должны быть полностью насыщены с учётом его арности.

6.4.10.2.2. Объявления экземпляров типов

Объявления экземпляров семейств типов очень похожи на стандартные объявления синонимов типов. Различий всего два: за ключевым словом type следует instance, а некоторые или все аргументы типа могут быть не переменными, но не могут содержать типы forall или семейства синонимов типов. Однако семейства данных, как правило, разрешены, а синонимы типов допустимы, если они применены ко всем аргументам и раскрываются в допустимый тип, — это точно те же требования, что и для экземпляров данных. Например, экземпляр [e] для Elem выглядит так:

type instance Elem [e] = e

Аргументы типов можно заменять символами подчёркивания (_), если имена аргументов не имеют значения. Это равносильно записи переменных типов с уникальными именами. Неиспользуемые аргументы типов можно заменить или предварить символами подчёркивания, чтобы избежать предупреждений при включённом флаге -Wunused-type-patterns. Применяются те же правила, что и для объявлений экземпляров данных.

Как и в случае с объявлениями экземпляров данных, при включённом расширении ExplicitForAll переменные типов и родов можно явно связывать в объявлении экземпляра типа.

Объявления экземпляров семейств типов допустимы только при наличии в области видимости соответствующего объявления семейства — так же, как для экземпляров классов требуется, чтобы объявление класса было видимым. Кроме того, каждое объявление экземпляра должно соответствовать роду, заданному объявлением семейства, а число параметров типа в объявлении экземпляра должно совпадать с числом параметров типа в объявлении семейства. Наконец, правая часть экземпляра типа должна быть мономорфным типом (то есть не может содержать forall), а после раскрытия всех полностью насыщенных обычных синонимов типов в ней не должно оставаться никаких синонимов, кроме синонимов семейств.

6.4.10.2.3. Закрытые семейства типов

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

type family F a where
  F Int  = Double
  F Bool = Char
  F a    = String

При упрощении применения семейства типов уравнения закрытого семейства типов проверяются по порядку, сверху вниз. В этом примере мы объявляем экземпляр для F, при котором F Int упрощается до Double, F Bool упрощается до Char, а для любого другого типа a, про который известно, что он не является ни Int, ни Bool, F a упрощается до String. Обратите внимание, что в последнем случае GHC должен быть уверен, что a не может унифицироваться с Int или Bool. Если программист укажет в коде только F a, GHC не сможет упростить тип. Ведь впоследствии a может быть инстанцирован как Int.

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

type family R a where
  forall t a. R (t a) = [a]
  forall a.   R a     = a

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

В файле hs-boot закрытые семейства типов должны либо иметь те же уравнения, что и в исходном файле, либо можно использовать следующий синтаксис, чтобы опустить уравнения (обратите внимание на буквальное ..):

type family R a where ..

В этом случае закрытое семейство типов R, соответствующее этому объявлению «boot», может иметь в исходном файле hs любое число уравнений (в том числе ни одного). Дополнительные сведения о взаимно рекурсивных модулях с модулями hs-boot (включая семейства типов) см. в разделе Взаимно рекурсивные модули и файлы hs-boot.

6.4.10.2.4. Примеры семейств типов

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

type family F a :: Type
type instance F [Int]   = Int   -- OK!
type instance F String  = Char  -- OK!
type instance F (F a)   = a     -- WRONG: type parameter mentions a type family
type instance
  F (forall a. (a, b))  = b     -- WRONG: a forall type appears in a type parameter
type instance
  F Float = forall a.a          -- WRONG: right-hand side may not be a forall type
type family H a where          -- OK!
  H Int  = Int
  H Bool = Bool
  H a    = String
type instance H Char = Char    -- WRONG: cannot have instances of closed family
type family K a where          -- OK!

type family G a b :: Type -> Type
type instance G Int            = (,)     -- WRONG: must be two type parameters
type instance G Int Char Float = Double  -- WRONG: must be two type parameters

6.4.10.2.5. Совместимость и раздельность уравнений семейств типов

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

1. все соответствующие типы и неявные роды в шаблонах являются раздельными; или
2. два шаблона унифицируются, порождая подстановку, и правые части равны при этой подстановке.

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

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

type instance F Int = Bool
type instance F Int = Char

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

type instance F (a, Int) = [a]
type instance F (Int, b) = [b]   -- overlap permitted

type instance G (a, Int)  = [a]
type instance G (Char, a) = [a]  -- ILLEGAL overlap, as [Char] /= [Int]

Обратите внимание, что это условие совместимости не зависит от того, является семейство типов ассоциированным или нет, и касается не только согласованности, но и безопасности типов.

Для семейства типов с полиморфным родом роды проверяются на раздельность так же, как типы. Например, следующий вариант принимается:

type family J a :: k
type instance J Int = Bool
type instance J Int = Maybe

Эти экземпляры совместимы, поскольку они различаются неявным параметром рода: в первом используется Type, а во втором — Type -> Type.

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

type instance H x   x = Int
type instance H [x] x = Bool

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

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

type family F a where
  F Int = Bool
  F a   = Char

type family G a where
  G Int = Int
  G a   = a

В определении F два уравнения несовместимы: их шаблоны не являются раздельными, а правые части при этом не совпадают. Поэтому, прежде чем выбрать второе уравнение, GHC должен убедиться, что первое никогда не сможет примениться. Таким образом, тип F a не упрощается; только тип, например F Double, будет упрощён до Char. В G, напротив, два уравнения совместимы. Поэтому при рассмотрении второго уравнения GHC может проигнорировать первое. Так, G a будет упрощён до a.

Несовместимости между уравнениями закрытого семейства типов можно показывать в :info, если включён параметр -fprint-axiom-incomps.

Однако правила перекрытия в GHCi описаны в разделе Объявления типов, классов и другие объявления.

6.4.10.2.6. Разрешимость экземпляров синонимов типов

Чтобы гарантировать разрешимость вывода типов при наличии семейств типов, необходимо наложить ряд дополнительных ограничений на формирование объявлений экземпляров типов (ср. определение 5 («Ослабленные условия») из работы «Проверка типов с открытыми функциями типов»). Объявления экземпляров имеют общий вид:

type instance F t1 .. tn = t

причём для каждого применения семейства типов (G s1 .. sm) в t требуется, чтобы:

1. s1 .. sm не содержали конструкторов семейств типов;
2. общее число символов (конструкторов типов данных и переменных типов) в s1 .. sm было строго меньше, чем в t1 .. tn; и
3. для каждой переменной типа a, a встречалось в s1 .. sm не чаще, чем в t1 .. tn.

Эти ограничения легко проверить, и они обеспечивают завершение вывода типов. Однако их недостаточно для гарантии полноты вывода типов при наличии так называемых «зацикливающихся равенств», например a ~ [F a], где рекурсивное вхождение переменной типа находится под применением семейства типов и конструктора типа данных. Подробности см. в упомянутой выше статье.

Если компилятору передан параметр UndecidableInstances (см. раздел Неразрешимые экземпляры и зацикливающиеся суперклассы), указанные выше ограничения не применяются, и программист сам отвечает за завершение нормализации семейств типов во время вывода типов.

6.4.10.2.7. Сведение применений семейств типов

-ffamily-application-cache

Флаг -ffamily-application-cache (включён по умолчанию) указывает GHC использовать кэш при сведении применений семейств типов. В большинстве случаев это ускоряет компиляцию. Использование этого флага не влияет на поведение программы во время выполнения.

Когда GHC встречает в программе применение семейства типов (например, F Int a), ему часто требуется свести его, чтобы завершить проверку типов. Вот простой пример:

type family F a where
  F Int            = Bool
  F (Maybe Double) = Char

g :: F Int -> Bool
g = not

Несмотря на то что тип g содержит F Int, GHC должен распознать, что аргумент g на самом деле имеет тип Bool. Для этого F Int сводится к Bool. Иногда информации для сведения применения семейства типов недостаточно; такое применение называется застрявшим. Продолжая этот пример, вхождение F (Maybe a) (для некоторой переменной типа a) застряло бы, поскольку ни одно уравнение не подходит.

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

Чтобы ускорить сведение семейств типов, GHC обычно использует кэш, запоминая, какие применения семейств типов он уже сводил. Эту возможность можно отключить с помощью -fno-family-application-cache.

6.4.10.4.1. Связанные экземпляры

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

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...

instance Eq (Elem [e]) => Collects [e] where
  type Elem [e] = e
  ...

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

class Collects ce where
  type Elem ce :: Type

instance Eq (Elem [e]) => Collects [e] where
  -- Choose one of the following alternatives:
  type Elem [e] = e       -- OK
  type Elem [x] = x       -- BAD; '[x]' is different to '[e]' from head
  type Elem x   = x       -- BAD; 'x' is different to '[e]'
  type Elem [Maybe x] = x -- BAD: '[Maybe x]' is different to '[e]'

Обратите внимание на следующие моменты:

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

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

  data family Nat :: k -> k -> Type
  -- k is implicitly bound by an invisible kind pattern
  newtype instance Nat :: (k -> Type) -> (k -> Type) -> Type where
    Nat :: (forall xx. f xx -> g xx) -> Nat f g
  
  class Funct f where
    type Codomain f :: Type
  instance Funct ('KProxy :: KProxy o) where
    -- o is implicitly bound by the kind signature
    -- of the LHS type pattern ('KProxy)
    type Codomain 'KProxy = NatTr (Proxy :: o -> Type)
  

• В экземплярах классов можно опустить экземпляр связанного типа. В этом случае, если для него нет экземпляра по умолчанию (см. Экземпляры связанных синонимов типов по умолчанию), соответствующий тип экземпляра не имеет значений; то есть этот тип могут иметь только расходящиеся выражения, например undefined.

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

  instance GMapKey Flob where
    data GMap Flob [v] = G1 v
    data GMap Flob Int = G2 Int
    ...
  

  Здесь мы объявляем два экземпляра данных: в одном последний параметр равен [v], а в другом — Int. Поскольку для (GMap Flob ...) нельзя объявить никаких последующих экземпляров, эта возможность наиболее полезна, когда свободный индексируемый параметр имеет вид с конечным числом вариантов (в отличие от Type).

• Если включено расширение ExplicitForAll, переменные типов и видов можно явно связывать в экземплярах связанных семейств данных или типов так же (и с теми же ограничениями), как в Объявлениях экземпляров данных или Объявлениях экземпляров типов. Например, следующий вариант приведённого выше кода будет принят:

  instance Eq (Elem [e]) => Collects [e] where
    type forall e. Elem [e] = e
  

6.4.10.4.2. Экземпляры связанных синонимов типов по умолчанию

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

class IsBoolMap v where
  type Key v
  type instance Key v = Int

  lookupKey :: Key v -> v -> Maybe Bool

instance IsBoolMap [(Int, Bool)] where
  lookupKey = lookup

В объявлении instance для класса, если для связанного типа не указано явное объявление type instance, вместо него используется объявление по умолчанию, как и в случае методов класса по умолчанию.

Обратите внимание на следующие моменты:

• Ключевое слово instance необязательно.
• Для связанного синонима типов можно указать не более одного объявления по умолчанию.
• Объявление по умолчанию не допускается для связанного типа данных.

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

  Как и в случае Связанных экземпляров, переменные типов и видов можно явно связывать в объявлениях по умолчанию с помощью forall, используя языковое расширение ExplicitForAll.

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

Вот несколько примеров:

class C (a :: Type) where
  type F1 a :: Type
  type instance F1 a = [a]     -- OK
  type instance F1 a = a->a    -- BAD; only one default instance is allowed

  type F2 b a                  -- OK; note the family has more type
                               --     variables than the class
  type instance F2 c d = c->d  -- OK; you don't have to use 'a' in the type instance

  type F3 a
  type F3 [b] = b              -- BAD; only type variables allowed on the
                               --      LHS, and the argument to F3 is
                               --      instantiated to [b], which is not
                               --      a bare type variable

  type F4 x y
  type F4 x x = x              -- BAD; the type variable x is repeated on
                               --      the LHS

  type F5 a
  type F5 b = a                -- BAD; 'a' is not in scope  in the RHS

  type F6 a :: [k]
  type F6 a = ('[] :: [x])     -- OK; the kind variable x is implicitly
                               --     bound by an invisible kind pattern
                               --     on the LHS

  type F7 a
  type F7 a =
    Proxy ('[] :: [x])         -- BAD; the kind variable x is not bound,
                               --      even by an invisible kind pattern

  type F8 (x :: a) :: [a]
  type F8 x = ('[] :: [a])     -- OK; the kind variable a is implicitly
                               --     bound by the kind signature of the
                               --     LHS type pattern

  type F9 (a :: k)
  type F9 a = Maybe a          -- BAD; the kind variable k is
                               --      instantiated to Type, which is not
                               --      a bare kind variable

  type F10 (a :: j) (b :: k)
  type F10 (a :: z) (b :: z)
    = Proxy a                  -- BAD; the kind variable z is repeated,
                               --      as both j and k are instantiated to z

  type F11 a b
  type forall a b. F11 a b = a -- OK; LHS type variables can be
                               --     explicitly bound with 'forall'

  type F12 (a :: k)
  type F12 @k a = Proxy a      -- OK; visible kind application syntax is
                               --     permitted in default declarations

6.4.10.4.3. Область видимости параметров класса

Видимость параметров класса в правой части экземпляров связанных семейств зависит исключительно от параметров семейства. Рассмотрим простой пример объявления класса:

class C a b where
  data T a

Параметром семейства данных является только один из двух параметров класса. Поэтому следующее объявление экземпляра недопустимо:

instance C [c] d where
  data T [c] = MkT (c, d)    -- WRONG!!  'd' is not in scope

Здесь в правой части экземпляра данных упоминается переменная типа d, которой нет в его левой части. Такие экземпляры данных недопустимы, поскольку они нарушили бы безопасность типов.

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

class C k where
  type T :: k

instance C (Maybe a) where
  type T = (Nothing :: Maybe a)

Здесь, хотя в правой части (Nothing :: Maybe a) упоминается переменная вида a, которой нет в левой части, это допустимо, поскольку a неявно связана шаблоном вида T.

Переменную вида также можно неявно связать в шаблоне типа в левой части, как в следующем примере:

class C a where
  type T (x :: a) :: [a]

instance C (Maybe a) where
  type T x = ('[] :: [Maybe a])

В ('[] :: [Maybe a]) переменная вида a неявно связана сигнатурой вида шаблона типа x в левой части.

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

Объявления экземпляров связанных типов и данных не наследуют контекст, указанный для охватывающего их экземпляра. Для объявлений экземпляров типов неясно, что означал бы такой контекст. В случае объявлений экземпляров данных маловероятно, что пользователь захочет повторять контекст для каждого конструктора данных. Единственное место, где контекст может быть полезен, — это предложение deriving связанного экземпляра данных. Однако даже здесь назначение контекста внешнего экземпляра не вполне ясно. Поэтому для простоты будем придерживаться приведённого выше правила: контекст охватывающего экземпляра игнорируется. Если для производного экземпляра нужен нетривиальный контекст, используйте предложение standalone deriving (на верхнем уровне).

6.4.10.5.1. Примеры

Вспомним наш пример класса GMapKey:

class GMapKey k where
  data GMap k :: Type -> Type
  insert :: GMap k v -> k -> v -> GMap k v
  lookup :: GMap k v -> k -> Maybe v
  empty  :: GMap k v

instance (GMapKey a, GMapKey b) => GMapKey (Either a b) where
  data GMap (Either a b) v = GMapEither (GMap a v) (GMap b v)
  ...method declarations...

Вот несколько списков экспорта и их значение:

• module GMap( GMapKey )
  

  Экспортирует только имя класса.

• module GMap( GMapKey(..) )
  

  Экспортирует класс, связанный тип GMap и функции-члены empty, lookup и insert. Конструкторы данных GMap (в данном случае GMapEither) не экспортируются.

• module GMap( GMapKey( type GMap, empty, lookup, insert ) )
  

  То же, что и в предыдущем пункте. Обратите внимание на ключевое слово «type».

• module GMap( GMapKey(..), GMap(..) )
  

  То же, что и в предыдущем пункте, но также экспортируются все конструкторы данных для GMap, а именно GMapEither.

• module GMap ( GMapKey( empty, lookup, insert), GMap(..) )
  

  То же, что и в предыдущем пункте.

• module GMap ( GMapKey, empty, lookup, insert, GMap(..) )
  

  То же, что и в предыдущем пункте.

Следует учитывать два момента:

• Нельзя написать GMapKey(type GMap(..)) — то есть спецификации подкомпонентов нельзя вкладывать друг в друга. Чтобы указать конструкторы данных GMap, его нужно перечислить отдельно.

• Рассмотрим следующий пример:

  module X where
    data family D
  
  module Y where
    import X
    data instance D Int = D1 | D2
  

  Модуль Y экспортирует все сущности, определённые в Y, а именно конструкторы данных D1 и D2, а также неявно семейство данных D, несмотря на то, что оно определено в X. Это означает, что можно написать import Y( D(D1,D2) ) без явного списка экспорта, например так:

       module Y( D(..) ) where ...
  or   module Y( module Y, D ) where ...
  

6.4.10.5.2. Экземпляры

Экземпляры семейств экспортируются неявно, как и экземпляры классов. Однако это относится только к заголовкам экземпляров, а не к определяемым ими конструкторам данных.

6.4.10.7.1. Синтаксис аннотации инъективности

Аннотация инъективности добавляется после заголовка семейства типов и состоит из двух частей:

• Переменная типа, обозначающая результат семейства типов. Синтаксис: = tyvar или = (tyvar :: kind). Переменная типа должна быть новой.
• Аннотация инъективности вида | A -> B, где A — переменная типа результата (см. предыдущий пункт), а B — список аргументов — переменных типов и видов, для которых семейство типов инъективно. Некоторые переменные можно опустить, если семейство типов не инъективно по ним.

Примеры:

type family Id a = result | result -> a where
type family F a b c = d | d -> a c b
type family G (a :: k) b c = foo | foo -> k b where

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

6.4.10.7.2. Проверка аннотации инъективности по уравнениям семейства типов

После того как пользователь объявляет семейство типов инъективным, GHC должен проверить корректность этого объявления, то есть убедиться, что уравнения семейства типов не нарушают аннотацию инъективности. Общая идея такова: если хотя бы одно уравнение (пункты (1), (2) и (3) ниже) или пара уравнений (пункты (4) и (5) ниже) нарушает аннотацию инъективности, семейство типов не является инъективным так, как утверждает пользователь, и сообщается об ошибке. В приведённых ниже пунктах правая часть означает правую часть уравнения семейства типов, инъективность которого проверяется. Левая часть означает аргументы этого уравнения семейства типов. Ниже перечислены правила, по которым проверяется инъективность семейства типов:

1. Если правая часть уравнения семейства типов является применением семейства типов, GHC сообщает, что семейство типов не является инъективным.
2. Если правая часть уравнения семейства типов — простая переменная типа, требуется, чтобы все переменные левой части (включая неявные переменные видов) также были простыми. Иными словами, это должно быть единственное уравнение данного семейства типов, охватывающее все возможные шаблоны. Если шаблоны не охватывают все варианты, GHC сообщает, что семейство типов не является инъективным.
3. Если переменная типа из левой части, объявленная инъективной, не упоминается в инъективной позиции правой части, GHC сообщает, что семейство типов не является инъективным. Инъективная позиция — это либо аргумент конструктора типа, либо инъективный аргумент семейства типов. Вывод типов может зациклиться при анализе применений инъективных семейств типов в правой части, поэтому для этого требуется UndecidableInstances; когда это необходимо, GHC предлагает включить это расширение.

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

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

5. В закрытом семействе типов все уравнения упорядочены и находятся в одном месте. Уравнения также проверяются попарно, но в этот раз каждое уравнение сопоставляется со всеми предшествующими уравнениями. Разумеется, закрытое семейство типов с единственным уравнением тривиально инъективно (если не выполняется условие (1), (2) или (3), приведённое выше).

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

Обратите внимание, что для проверки инъективности в пунктах (4) и (5) GHC использует специальный вариант алгоритма унификации, который рассматривает применения семейств типов как потенциально унифицируемые с чем угодно.