6.10.4. Квантифицированные ограничения

6.10.4.1. Мотивация

Введение квантифицированных ограничений предоставляет две основные выгоды:

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

  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 Derivable type classes.

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
  

  См. резюме Айсленда Джека. Суть в том, что часть справа от => может быть заголовком переменной типа (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).

Короче говоря, квантифицированные ограничения не вводят несогласованность.