6.10.4. Ограничения с кванторами

6.10.4.1. Мотивация

Введение ограничений с кванторами даёт два основных преимущества:

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

  data Rose f x = Rose x (f (Rose f x))
  
  instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where
    (Rose x1 rs1) == (Rose x2 rs2) = x1 == x2 && rs1 == rs2
  

  Это расширение позволяет записывать ограничения вида forall b. Eq b => Eq (f b), необходимые для разрешения ограничения Eq (f (Rose f x)), возникающего при втором использовании метода (==).

• Во-вторых, ограничения с кванторами позволяют задавать более краткие и точные спецификации. Например, рассмотрим класс типов MTL для монадных трансформеров:

  class Trans t where
    lift :: Monad m => m a -> (t m) a
  

  Разработчику известно, что монадный трансформер преобразует монаду m в новую монаду t m. Но это свойство формально не указано в приведённом выше объявлении. Это упущение становится проблемой при определении композиции монадных трансформеров:

  newtype (t1 * t2) m a = C { runC :: t1 (t2 m) a }
  
  instance (Trans t1, Trans t2) => Trans (t1 * t2) where
    lift = C . lift . lift
  

  Здесь требуется lift от монады m к t2 m, а затем снова lift в t1 (t2 m). Однако этот второй lift можно принять, только если (t2 m) является монадой, а установить, что это свойство выполняется всегда, невозможно.

  Ограничения с кванторами позволяют явно указать это свойство в объявлении класса Trans:

  class (forall m. Monad m => Monad (t m)) => Trans t where
    lift :: Monad m => m a -> (t m) a
  

Эта идея появилась очень давно; см. раздел 7 статьи Выводимые классы типов.

6.10.4.2. Изменения синтаксиса

В Haskell 2010 context (часть типа слева от =>) определяется так:

context ::= class
        |   ( class1, ..., classn )

class ::= qtycls tyvar
        |  qtycls (tyvar atype1 ... atypen)

Мы расширяем class (предупреждение: это название нетерминального символа может сбить с толку) двумя дополнительными формами — именно теми, которые могут встречаться в объявлении экземпляра:

class ::= ...
      | [context =>] qtycls inst
      | [context =>] tyvar inst

Определение inst не изменяется по сравнению с отчётом Haskell (в общих чертах — это просто тип). Часть context => необязательна. Это единственное синтаксическое изменение языка.

Примечания:

• Везде, где GHC допускает расширения в объявлениях экземпляров, мы допускаем те же расширения и для этой новой формы class. В частности, с ExplicitForAll и MultiParamTypeClasses синтаксис будет таким:

  class ::= ...
         | [forall tyvars .] [context =>] qtycls inst1 ... instn
         | [forall tyvars .] [context =>] tyvar inst1 ... instn
  

  Обратите внимание, что явное forall часто совершенно необходимо. Рассмотрим пример с розовым деревом:

  instance (Eq a, forall b. Eq b => Eq (f b)) => Eq (Rose f a) where ...
  

  Без forall b переменная типа b квантифицировалась бы во всём объявлении экземпляра, что не соответствует замыслу.

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

  f :: (Eq a, forall b. Eq b => Eq (f b)) => Rose f a -> Rose f a -> Bool
  f t1 t2 = not (t1 == t2)
  

• Форма с переменной типа в заголовке позволяет написать следующее:

  instance (forall xx. c (Free c xx)) => Monad (Free c) where
      Free f >>= g = f g
  

  См. краткое изложение Iceland Jack. Ключевой момент в том, что часть справа от => может начинаться с переменной типа (в данном случае c), а не с класса. Однако это не должна быть одна из переменных, связанных квантором forall.

  (Примечание: это выходит за рамки описанного в статье, но, по-видимому, не создаёт новых технических сложностей.)

6.10.4.3. Изменения типизации

См. статью.

6.10.4.4. Суперклассы

Предположим, у нас есть:

f :: forall m. (forall a. Ord a => Ord (m a)) => m Int -> Bool
f x = x == x

Для x==x нам требуется ограничение Eq (m Int), но контекст позволяет нам получать только ограничения Ord (m a). Однако из заданного ограничения forall a. Ord a => Ord (m a) мы выводим второе заданное ограничение forall a. Ord a => Eq (m a), а с его помощью легко разрешаем Eq (m Int). Этот процесс очень похож на уже существующий механизм суперклассов: из заданного ограничения Ord a мы выводим второе заданное ограничение Eq a.

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

6.10.4.5. Перекрытие

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

class A a where {}
class B a where {}
class C a where {}
class (A a => C a) => D a where {}
class (B a => C a) => E a where {}

class C a => F a where {}
instance (B a, D a, E a) => F a where {}

При проверке типов объявления экземпляра F a нам нужно проверить, выполняется ли суперкласс C для F. Поэтому мы пытаемся вывести ограничение C a в теории, содержащей:

• Аксиомы экземпляров: (B a, D a, E a) => F a
• Локальные аксиомы из контекста экземпляра: B a, D a и E a
• Замыкание отношения суперклассов для этих локальных аксиом: A a => C a и B a => C a

Однако обе аксиомы A a => C a и B a => C a подходят к требуемому ограничению C a. Есть несколько возможных способов обработки таких перекрывающихся локальных аксиом:

• Выбрать первую. Можно просто выбрать первую подходящую аксиому. В приведённом выше примере это будет A a => C a. Затем нам нужно вывести A a, для которого нет подходящих аксиом, поэтому приведённая программа будет отклонена.

  Но предположим, что мы немного изменили порядок ограничений в контексте экземпляра, поместив E a перед D a:

  instance (B a, E a, D a) => F a where {}
  

  Первая подходящая аксиома, которую мы встречаем при выводе C a, — это B a => C a. У нас есть локальная аксиома B a, поэтому теперь программа внезапно принимается. Такое поведение, при котором порядок ограничений в контексте экземпляра определяет, будет ли программа принята, кажется разработчику довольно запутанным.

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

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

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

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

6.10.4.6. Поиск экземпляра

С учётом решения о перекрытии поиск экземпляра при попытке разрешить ограничение класса C t работает следующим образом:

1. Сначала проверяем, есть ли заданное ограничение без кванторов C t. Если есть, используем его для разрешения ограничения.
2. Если нет, рассматриваем все доступные заданные ограничения с кванторами; если ровно одно из них подходит к C t, выбираем его; если подходит несколько, выдаём ошибку.
3. Если ни одно ограничение с кванторами не подходит, ищем среди глобальных экземпляров, как описано в разделах Объявления экземпляров и их разрешение и Перекрывающиеся экземпляры.

6.10.4.7. Завершение

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

• Каждое ограничение с квантором, взятое отдельно, должно удовлетворять правилам завершения для объявления экземпляра.
• После фразы «для каждого ограничения класса (C t1 ... tn)» добавьте «или для каждого ограничения с квантором (forall as. context => C t1 .. tn)».

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

Разумеется, UndecidableInstances снимает ограничения условий Патерсона, как и сейчас.

6.10.4.8. Когерентность

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

f :: (forall a. Eq a => Eq (f a)) => f b -> f Bool
f x = ...rhs...

В ...rhs... фактически присутствует локальный экземпляр Eq (f a) для любого a. Но в месте вызова f компилятор сам создаёт свидетельство, передаваемое в f. Например, если вызвать f Nothing, то f — это Maybe, и компилятор должен доказать (в месте вызова), что выполняется forall a. Eq a => Eq (Maybe a). Это легко сделать, сославшись на существующее объявление экземпляра для Eq (Maybe a).

Иными словами, ограничения с кванторами не приводят к некогерентности.