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 для инстанса
• Самостоятельные типовые подписи для полиморфной рекурсии
• Типовые подписи для конструкторов обобщенных алгебраических типов данных (GADTs)
• Типовые подписи для псевдонимов шаблонов
• Объявления инстансов данных, Объявления типовых инстансов, Закрытые типы семейств и Связанные инстансы
• Правила переписывания, в которых переменные типов явно квантифицированы

Примечания:

• Типовые подписи шаблонов — заметный пример того, где типы не подчиняются правилу «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. См. Формальный синтаксис для GADTs.