6.8.8. Объявления и разрешение экземпляров

6.8.8.1. Упрощённые правила для заголовка экземпляра

TypeSynonymInstances

Следует из:

FlexibleInstances

С:

6.8.1

Статус:

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

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

FlexibleInstances

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

TypeSynonymInstances

С:

6.8.1

Статус:

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

Позволяет определять экземпляры типов классов с произвольными вложенными типами в заголовке экземпляра.

В Haskell 2010 заголовок объявления экземпляра должен иметь вид C (T a1 ... an), где T — конструктор типа данных, а a1 ... an — различные переменные типа. В случае многопараметрических типов классов это правило применяется к каждому параметру заголовка экземпляра (можно было бы позволить только одному параметру иметь этот вид, а другие быть переменными типов, но на данный момент это правила).

GHC ослабляет это правило двумя способами:

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

  type Point a = (a,a)
  instance C (Point a) where ...
  

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

  instance C (a,a) where ...
  

  Как и раньше, синонимы типов должны быть полностью применены. Например, нельзя написать:

  instance Monad Point where ...
  

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

  instance C (Maybe Int) where ...
  

  См. также правила перекрытия.

  Расширение FlexibleInstances подразумевает TypeSynonymInstances.

Однако объявление экземпляра все еще должно соответствовать правилам завершения экземпляра: см. Правила завершения экземпляров.

6.8.8.2. Формальная синтаксис для типов объявлений экземпляров

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

inst_top ::= 'instance' opt_forall opt_ctxt inst_head opt_where

opt_forall ::= <empty>
            |  'forall' tv_bndrs '.'

tv_bndrs ::= <empty>
          |  tv_bndr tv_bndrs

tv_bndr ::= tyvar
         |  '(' tyvar '::' ctype ')'

opt_ctxt ::= <empty>
          |  btype '=>'
          |  '(' ctxt ')' '=>'

ctxt ::= ctype
      |  ctype ',' ctxt

inst_head ::= '(' inst_head ')'
           |  prefix_cls_tycon arg_types
           |  arg_type infix_cls_tycon arg_type
           |  '(' arg_type infix_cls_tycon arg_type ')' arg_types

arg_types ::= <empty>
           |  arg_type arg_types

opt_where ::= <empty>
           |  'where'

Где:

• btype — тип, который не может иметь внешний forall/=> , если он не заключён в скобки. Например, forall a. a и Eq a => a не являются допустимыми btype , но (forall a. a) и (Eq a => a) допустимы.
• ctype — btype , у которого нет ограничений на внешний forall/=>, поэтому forall a. a и Eq a => a являются допустимыми ctype.
• arg_type — тип, который не может иметь forall или =>
• prefix_cls_tycon — конструктор типа класса, написанный префиксом (например, Show или (&&&)), а infix_cls_tycon — конструктор типа класса, написанный инфикс (например, \`Show\` или &&&).

Это упрощённая грамматика, которая не полностью рассматривает все детали реализации парсера GHC (например, размещение комментариев Haddock), но её достаточно для понимания того, что синтаксически разрешено. Некоторые дополнительные наблюдения по этой грамматике:

• Объявления экземпляров не могут быть объявлены с вложенными forall или => . Например, это будет отклонено:

  instance forall a. forall b. C (Either a b) where ...
  

  В результате inst_top размещает все квантификации и ограничения впереди opt_forall и opt_context.

• Кроме того, типы объявлений экземпляров не допускают внешних скобок, окружающих opt_forall или opt_ctxt, если хотя бы один из них используется. Например, instance (forall a. C a) будет отклонено, так как GHC будет рассматривать forall как вложенный.

  Обратите внимание, что использование скобок в inst_head допустимо. Например, instance (C a) принимается, как и instance forall a. (C a).

6.8.8.3. Правила завершения экземпляров

Независимо от FlexibleInstances и FlexibleContexts, объявления экземпляров должны соответствовать некоторым правилам, которые гарантируют, что разрешение экземпляров завершится. Ограничения могут быть сняты с помощью UndecidableInstances (см. Неразрешимые экземпляры и циклические надклассы).

Эти правила таковы:

1. Условия Патерсона: для каждого ограничения класса (C t1 ... tn) в контексте

   1. Ни одна переменная типа не имеет больше вхождений в ограничение, чем в заголовке
   2. Ограничение имеет меньше конструкторов и переменных (взятых вместе и учитывая повторения), чем заголовок
   3. Ограничение не упоминает функции типов. Применение функции типа, в принципе, может расшириться до типа произвольного размера, и поэтому они отклоняются сразу

   Если эти три условия выполняются, мы говорим, что ограничение (C t1 ... tn) меньше Патерсона, чем заголовок экземпляра.

2. Условие покрытия. Для каждой функциональной зависимости ⟨tvs⟩_left -> ⟨tvs⟩_right класса, каждая переменная типа в S(⟨tvs⟩_right) должна появляться в S(⟨tvs⟩_left), где S — подстановка, отображающая каждую переменную типа в объявлении класса на соответствующий тип в заголовке экземпляра.

Эти ограничения гарантируют завершение разрешения экземпляров: каждый шаг сокращения делает задачу меньше по крайней мере на один конструктор. Вы можете найти много справочных материалов о причинах этих ограничений в статье Understanding functional dependencies via Constraint Handling Rules.

Например, это допустимо:

instance C Int [a]          -- Multiple parameters
instance Eq (S [a])         -- Structured type in head

    -- Repeated type variable in head
instance C4 a a => C4 [a] [a]
instance Stateful (ST s) (MutVar s)

    -- Head can consist of type variables only
instance C a
instance (Eq a, Show b) => C2 a b

    -- Non-type variables in context
instance Show (s a) => Show (Sized s a)
instance C2 Int a => C3 Bool [a]
instance C2 Int a => C3 [a] b

Но это нет:

    -- Context assertion no smaller than head
instance C a => C a where ...
    -- (C b b) has more occurrences of b than the head
instance C b b => Foo [b] where ...

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

data MinHeap h a = H a (h a)
  deriving (Show)

потому что производный экземпляр

instance (Show a, Show (h a)) => Show (MinHeap h a)

соответствует вышеперечисленным правилам.

Ограничения на функциональные зависимости (Функциональные зависимости) особенно проблематичны. Искушение заключается в введении переменных типа в контексте, которые не появляются в заголовке, что исключено обычными правилами. Например:

class HasConverter a b | a -> b where
   convert :: a -> b

data Foo a = MkFoo a

instance (HasConverter a b,Show b) => Show (Foo a) where
   show (MkFoo value) = show (convert value)

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

class D a
class F a b | a->b
instance F [a] [[a]]
instance (D c, F a c) => D [a]   -- 'c' is not mentioned in the head

Аналогично, может возникнуть желание снять ограничение покрытия:

class Mul a b c | a b -> c where
  (.*.) :: a -> b -> c

instance Mul Int Int Int where (.*.) = (*)
instance Mul Int Float Float where x .*. y = fromIntegral x * y
instance Mul a b c => Mul a [b] [c] where x .*. v = map (x.*.) v

Третье объявление экземпляра не удовлетворяет условию покрытия; и, действительно, следующее (довольно странное) определение:

f = \ b x y -> if b then x .*. [y] else y

заставляет вывод экземпляров зациклиться, потому что он требует ограничения (Mul a [b] b).

6.8.8.4. Неразрешимые экземпляры и циклические суперклассы

UndecidableInstances

Since:

6.8.1

Разрешает определение экземпляров, которые могут привести к нетерминации проверки типов.

Расширение UndecidableInstances снимает ограничения на объявления экземпляров, описанные в Правилах завершения экземпляров. Расширение UndecidableInstances также снимает некоторые ограничения, наложенные на экземпляры семейств типов; см. Разрешимость экземпляров синонимов типов.

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

class C a => D a where ...

instance Wombat [b] => D [b] where ...

При проверке типа этого instance объявления GHC должен гарантировать, что суперкласс (C [b]) экземпляра D удовлетворяется. Мы говорим, что (C [b]) является Требуемым ограничением суперкласса объявления экземпляра.

Если существует instance blah => C [b], что часто случается, GHC может использовать объявление экземпляра, и всё хорошо. Но предположим, что такого экземпляра нет, поэтому GHC может удовлетворить Требуемое (C [b]) только из контекста экземпляра, а именно, из данного ограничения (Wombat [b]). Возможно, объявление Wombat выглядит так:

class C a => Wombat a

Таким образом, у данного (Wombat [b]) есть суперкласс (C [b]), и похоже, что мы можем удовлетворить Требуемое (C [b]) ограничение из этого суперкласса Wombat. Но оказывается, что это может привести к тонким циклическим словарям, и GHC этого не допускает.

Правило таково: Требуемое ограничение суперкласса может быть удовлетворено только одним из следующих трёх способов:

1. Непосредственно из контекста объявления экземпляра. Например, если объявление выглядело так:

   instance (Wombat [b], C [b]) => D [b] where ...
   

   мы могли бы удовлетворить Требуемое (C [b]) из данного (C [b]).

2. Используя другое объявление экземпляра. Например, если у нас есть:

   instance C b => C [b] where ...
   

   мы можем удовлетворить Требуемое ограничение суперкласса (C [b]) с помощью этого экземпляра, сведя его к Требуемому ограничению (C b) (которое всё ещё нужно решить).

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

   • Ни одна переменная типа не может встречаться чаще в X, чем в заголовке экземпляра.
   • X должен содержать меньше конструкторов и переменных типов (взятых вместе, считая повторения), чем заголовок экземпляра.
   • X не должен упоминать функции типов.

Правило (3) — самое сложное. Вот пример, взятый из исходного кода GHC:

       class Ord r => UserOfRegs r a where ...
(i1)   instance UserOfRegs r a => UserOfRegs r (Maybe a) where
(i2)   instance (Ord r, UserOfRegs r CmmReg) => UserOfRegs r CmmExpr where

Для (i1) мы можем получить суперкласс (Ord r) путём выбора из (UserOfRegs r a), поскольку он (т.е. UserOfRegs r a) меньше, чем заголовок объявления экземпляра, а именно (UserOfRegs r (Maybe a)) по Патерсону.

Но для (i2) это не так: (UserOfRegs r CmmReg) не меньше по Патерсону, чем заголовок экземпляра (UserOfRegs r CmmExpr), поэтому мы не можем использовать суперклассы первого. Поэтому мы должны добавить явное и, возможно, неожиданное (Ord r) аргумент в объявление экземпляра.

Это исправление, заключающееся в простом добавлении, по-видимому, избыточного ограничения в контекст объявления экземпляра, надёжно работает: оно всегда решает проблему. (Мы рассматривали возможность автоматического добавления, но решили, что лучше оставить его явным.)

Исправление этой тонкой циклической зависимости суперклассов имеет долгую историю; если вас это интересует, прочтите Note [Recursive superclasses] и Note [Solving superclass constraints] в GHC.Tc.TyCl.Instance.

6.8.8.5. Перекрывающиеся экземпляры

OverlappingInstances

Since:

6.8.1

Status:

Устаревшее

Устаревшее расширение для ослабления проверок, предназначенных для обеспечения завершения разрешения экземпляров.

IncoherentInstances

Implies:

OverlappingInstances.

Since:

6.8.1

Status:

Устаревшее

Устаревшее расширение для ослабления проверок, предназначенных для обеспечения завершения разрешения экземпляров.

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

Для управления выбором экземпляра можно указать поведение перекрытия для отдельных экземпляров с помощью псевдонима, написанного непосредственно после ключевого слова instance. Псевдоним может быть одним из: {-# OVERLAPPING #-}, {-# OVERLAPPABLE #-}, {-# OVERLAPS #-}, или {-# INCOHERENT #-}.

Поведение соответствия также зависит от двух флагов языка модульного уровня: OverlappingInstances и IncoherentInstances. Эти расширения теперь устарели (начиная с GHC 7.10) в пользу мелкозернистых псевдонимов для каждого экземпляра.

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

• Экземпляр является несовместимым, если: у него есть псевдоним INCOHERENT; или если у экземпляра нет псевдонима, и он появляется в модуле, скомпилированном с IncoherentInstances.
• Экземпляр является перекрываемым, если: у него есть псевдоним OVERLAPPABLE или OVERLAPS; или если у экземпляра нет псевдонима, и он появляется в модуле, скомпилированном с OverlappingInstances; или если экземпляр является несовместимым.
• Экземпляр является перекрывающимся, если: у него есть псевдоним OVERLAPPING или OVERLAPS; или если у экземпляра нет псевдонима, и он появляется в модуле, скомпилированном с OverlappingInstances; или если экземпляр является несовместимым.

Теперь предположим, что в некотором клиентском модуле мы ищем экземпляр целевого ограничения (C ty1 .. tyn). Поиск работает следующим образом:

• Найдите все экземпляры \(I\), которые соответствуют целевому ограничению; то есть целевое ограничение является экземпляром подстановки \(I\). Эти объявления экземпляров являются кандидатами.
• Если не осталось кандидатов, поиск завершается неудачей

• Удалите любого кандидата \(IX\), для которого существует другой кандидат \(IY\) такой, что выполняются оба следующих условия:

  • \(IY\) строго более специфичен, чем \(IX\). То есть \(IY\) является экземпляром подстановки \(IX\), но не наоборот.
  • \(IX\) является перекрываемым или \(IY\) является перекрывающимся. (Эта конструкция «или», а не «и», позволяет клиенту намеренно перезаписывать экземпляр из библиотеки без необходимости изменения библиотеки.)
• Если все оставшиеся кандидаты несовместимы, поиск завершается успехом, возвращая произвольного выжившего кандидата.
• Если остаётся более одного несовместимого кандидата, поиск завершается неудачей.
• В противном случае остаётся ровно один несовместимый кандидат; назовём его «главным кандидатом».
• Теперь найдите все экземпляры или входящие ограничения, которые унифицируют с целевым ограничением, но не соответствуют ему. Такие не-кандидатные экземпляры могут соответствовать, когда целевое ограничение дополнительно инстанцируется. Если все они являются несовместимыми экземплярами верхнего уровня, поиск завершается успехом, возвращая главного кандидата. В противном случае поиск завершается неудачей.

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

Ошибки сообщаются лениво (при попытке решить ограничение), а не жадно (когда определяются сами экземпляры). Рассмотрим, например

instance C Int  b where ..
instance C a Bool where ..

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

В качестве более существенного примера применения правил рассмотрим

instance {-# OVERLAPPABLE #-} context1 => C Int b     where ...  -- (A)
instance {-# OVERLAPPABLE #-} context2 => C a   Bool  where ...  -- (B)
instance {-# OVERLAPPABLE #-} context3 => C a   [b]   where ...  -- (C)
instance {-# OVERLAPPING  #-} context4 => C Int [Int] where ...  -- (D)

(Все они нуждаются в FlexibleInstances.) Теперь предположим, что движок вывода типов должен решить ограничение C Int [Int]. Это ограничение соответствует экземплярам (A), (C) и (D), но последний более специфичен и, следовательно, выбирается.

Если (D) не существует, то (A) и (C) всё ещё будут сопоставлены, но ни один из них не является наиболее специфичным. В этом случае программа будет отклонена, если не включено IncoherentInstances, в этом случае она будет принята, и (A) или (C) будут выбраны произвольно.

Объявление экземпляра более специфично, чем другое, если заголовок первого является экземпляром подстановки последнего. Например, (D) «более специфичен», чем (C), потому что вы можете перейти от (C) к (D) путём подстановки a := Int и b := Int.

Последний пункт (о унификации экземпляров) заставляет GHC быть консервативным при принятии перекрывающегося экземпляра. Например:

f :: [b] -> [b]
f x = ...

Предположим, что из правой части f мы получим ограничение C b [b]. Но GHC не берёт на себя обязательство по экземпляру (C), потому что в определённом вызове f, b может быть инстанцировано как Int, в этом случае экземпляр (D) был бы ещё более специфичным. Поэтому GHC отклоняет программу.

Однако, если вы включите расширение IncoherentInstances при компиляции модуля, содержащего (D), GHC вместо этого выберет (C) без каких-либо жалоб по поводу проблемы последующих инстанциаций.

Обратите внимание, что мы предоставили тип подписи для f, поэтому GHC должен был проверить, что f имеет указанный тип. Предположим вместо этого, что мы не предоставляем тип подписи, попросив GHC вместо этого вывести его. В этом случае GHC воздержится от упрощения ограничения C Int [b] (по той же причине, что и раньше), но вместо отклонения программы, он выведет тип

f :: C b [b] => [b] -> [b]

Это откладывает вопрос о выборе экземпляра до места вызова f, к тому времени будет известно больше о типе b. Вам понадобится расширение FlexibleContexts.

Точно такая же ситуация может возникнуть и в самих объявлениях экземпляров. Предположим, что у нас есть

class Foo a where
   f :: a -> a
instance Foo [b] where
   f x = ...

и, как и прежде, ограничение C Int [b] возникает из правой части f . GHC отклонит экземпляр, пожалуясь, как и прежде, что не знает, как разрешить ограничение C Int [b], потому что оно соответствует более чем одному объявлению экземпляра. Решением является отсрочка выбора путём добавления ограничения к контексту объявления экземпляра, таким образом:

instance C Int [b] => Foo [b] where
   f x = ...

(Вам нужно FlexibleContexts для этого.)

При проверке унификации в последнем пункте GHC также использует «ограничения, заданные в контексте». Рассмотрим, например

instance C a Int

g :: forall b c. C b Int => blah
g = ...needs (C c Int)...

Здесь GHC не будет решать ограничение (C c Int) из экземпляра верхнего уровня, потому что в конкретном вызове g оба b и c могут быть инстанцированы в один и тот же тип, что позволит решить ограничение другим способом. Это последнее ограничение в основном для того, чтобы сделать решатель ограничений полным. (Заинтересовавшиеся могут прочитать Note [Instance and Given overlap] в TcInteract.) Это легко избежать: в типе подписи избегайте ограничения, которые соответствуют экземпляру верхнего уровня. Флаг -Wsimplifiable-class-constraints предупреждает о таких подписях.

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

InstanceSigs

Since:

7.6.1

Статус:

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

Разрешает типы сигнатур для членов в определениях экземпляров.

Расширение InstanceSigs позволяет пользователям указывать типы сигнатур для методов класса в объявлении экземпляра класса. Например:

data T a = MkT a a
instance Eq a => Eq (T a) where
  (==) :: T a -> T a -> Bool   -- The instance signature
  (==) (MkT x1 x2) (MkTy y1 y2) = x1==y1 && x2==y2

Некоторые детали:

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

  instance Eq a => Eq (T a) where
     (==) :: forall b. b -> b -> Bool
     (==) x y = True
  

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

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

  instance Eq (T Int) where
    (==) :: Eq Int => T Int -> T Int -> Bool
    (==) (MkT x1 _) (MkT y1 _) = x1 == y1
  

  Ограничение Eq Int в сигнатуре экземпляра будет решено с помощью экземпляра верхнего уровня Eq Int, из чего следует, что сигнатура экземпляра действительно так же общая, как и тип инстанцированного метода класса T Int -> T Int -> Bool.

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

• Подпись экземпляра чисто локальна для объявления экземпляра класса. Она влияет только на проверку типа метода в экземпляре; она не влияет на что-либо за пределами экземпляра класса. Таким образом, она похожа на встроенную сигнатуру типа:

  instance Eq a => Eq (T a) where
      (==) = (\ x y -> True) :: forall b. b -> b -> Bool
  

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

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

  class C a where
    foo :: b -> a -> (a, [b])
  
  instance C a => C (T a) where
    foo :: forall b. b -> T a -> (T a, [b])
    foo x (T y) = (T y, xs)
       where
         xs :: [b]
         xs = [x,x,x]
  

  При условии, что вы также указали ScopedTypeVariables (Переменные типа со сферой действия), forall b охватывает определение foo, а в частности, сигнатуру типа для xs.