6.11.1. Явная универсальная квантификация (forall)

6.11.1.1. Правило «forall или ничего»

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

f  :: forall a b. a -> b -> b         -- OK, `a` and `b` are explicitly bound
g  :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound
h  :: forall a. a -> b -> b           -- Rejected, `b` is not in scope

Сигнатуры типов для f, g и h начинаются с внешнего невидимого forall, поэтому каждая переменная типа в этих сигнатурах должна быть явно связана с помощью forall. И f, и g соответствуют правилу «forall или ничего», поскольку в них явно квантифицируются a и b. С другой стороны, в h b явно не квантифицируется, поэтому GHC отклонит эту сигнатуру типа из-за неправильной области видимости.

В местах, где применяется правило «forall или ничего», если у типа нет внешнего невидимого forall, все переменные типов, не связанные явно с помощью forall, квантифицируются неявно. Например:

i :: a -> b -> b             -- `a` and `b` are implicitly quantified
j :: a -> forall b. b -> b   -- `a` is implicitly quantified
k :: (forall a. a -> b -> b) -- `b` is implicitly quantified
type L :: forall a -> b -> b -- `b` is implicitly quantified

GHC примет сигнатуры типов i, j и k, а также сигнатуру вида для L. Обратите внимание:

• Сигнатура j принимается, несмотря на сочетание неявной и явной квантификации. Пока forall не является внешним, его можно использовать среди неявно связанных переменных типов.
• Сигнатура k принимается, поскольку внешние скобки означают, что forall не является внешним forall. Правило «forall или ничего» — один из немногих случаев в GHC, когда наличие или отсутствие скобок может иметь семантическое значение!
• Сигнатура L начинается с внешнего forall, но это видимый forall, а не невидимый forall, поэтому правило «forall или ничего» не применяется.

Правило «forall или ничего» применяется в следующих местах:

• Объявления сигнатур типов функций, значений и методов классов
• Аннотации типов выражений
• Объявления экземпляров
• Сигнатуры методов по умолчанию
• Сигнатуры типов в прагме SPECIALIZE или прагме SPECIALIZE instance
• Самостоятельные сигнатуры видов и полиморфная рекурсия
• Сигнатуры типов конструкторов обобщённых алгебраических типов данных (GADT)
• Сигнатуры типов для синонимов шаблонов
• Объявления экземпляров данных, объявления экземпляров типов, закрытые семейства типов и ассоциированные экземпляры
• Правила переписывания, в которых переменные типов квантифицируются явно

Примечания:

• Сигнатуры типов шаблонов — примечательный пример места, где типы не подчиняются правилу «forall или ничего». Например, GHC примет следующий код:

  f (g :: forall a. a -> b) x = g x :: b
  

  Кроме того, правила переписывания не подчиняются правилу «forall или ничего», если их переменные типов не квантифицируются явно:

  {-# RULES "f" forall (g :: forall a. a -> b) x. f g x = g x :: b #-}
  

• Конструкторы GADT особенно требовательны к своим forall. Помимо соблюдения правила «forall или ничего», конструкторы GADT также запрещают вложенные forall. Например, GHC отклонит следующий GADT:

  data T where
    MkT :: (forall a. a -> b -> T)
  

  Из-за отсутствия внешнего forall в типе MkT переменная b квантифицировалась бы неявно. По сути, это было бы равносильно записи MkT :: forall b. (forall a. a -> b -> T), содержащей вложенные forall. См. Формальный синтаксис GADT.