6.11.5. Лексически ограниченные переменные типа

6.11.5.1. Обзор

В основу разработки положены следующие принципы

• Ограниченная переменная типа обозначает переменную типа, а не тип. (Это изменение по сравнению с прежним устройством GHC.)
• Кроме того, разные лексические переменные типа обозначают разные переменные типа. Это означает, что каждая написанная программистом сигнатура типа (в том числе содержащая свободные ограниченные переменные типа) задаёт жёсткий тип, то есть тип, полностью известный проверяющей типы системе, без участия вывода типов.
• Лексические переменные типа можно свободно переименовывать с точностью до альфа-переименования, не изменяя программу.

Лексически ограниченная переменная типа может быть связана:

• Сигнатурой типа объявления (сигнатуры типов объявлений)
• Сигнатурой типа выражения (сигнатуры типов выражений)
• Сигнатурой типа в образце (сигнатуры типов в образцах)
• Объявлениями классов и экземпляров (объявления классов и экземпляров)

В Haskell написанная программистом сигнатура типа неявно квантифицируется по свободным переменным типа (раздел 4.1.2 отчёта Haskell). Лексически ограниченные переменные типа влияют на правила этой неявной квантификации следующим образом: любая переменная типа, находящаяся в области видимости, не квантифицируется универсально. Например, если переменная типа a находится в области видимости, то

(e :: a -> a)     means     (e :: a -> a)
(e :: b -> b)     means     (e :: forall b. b->b)
(e :: a -> b)     means     (e :: forall b. a->b)

6.11.5.2. Сигнатуры типов объявлений

Сигнатура типа объявления, содержащая явную квантификацию (с помощью forall), вводит явно квантифицированные переменные типа в область видимости определения именованной функции. Например:

f :: forall a. [a] -> [a]
f (x:xs) = xs ++ [ x :: a ]

«forall a» вводит «a» в область видимости определения «f».

Это происходит только при соблюдении следующих условий:

• Квантификация в сигнатуре типа для f явная. Например:

  g :: [a] -> [a]
  g (x:xs) = xs ++ [ x :: a ]
  

  Эта программа будет отклонена, потому что «a» не распространяется на определение «g», поэтому согласно обычным правилам неявной квантификации Haskell «x::a» означает «x::forall a. a».

• Переменная типа квантифицируется единственным, синтаксически видимым внешним forall в сигнатуре типа. Например, GHC отклонит все следующие примеры:

  f1 :: forall a. forall b. a -> [b] -> [b]
  f1 _ (x:xs) = xs ++ [ x :: b ]
  
  f2 :: forall a. a -> forall b. [b] -> [b]
  f2 _ (x:xs) = xs ++ [ x :: b ]
  
  type Foo = forall b. [b] -> [b]
  
  f3 :: Foo
  f3 (x:xs) = xs ++ [ x :: b ]
  

  В f1 и f2 переменная типа b не квантифицируется внешним forall, поэтому она не находится в области видимости тел функций. Переменная b также не находится в области видимости тела f3, поскольку forall скрыт внутри синонима типа Foo.

• Сигнатура задаёт тип связывания функции или отдельного связывания переменной, но не связывания образца. Например:

  f1 :: forall a. [a] -> [a]
  f1 (x:xs) = xs ++ [ x :: a ]   -- OK
  
  f2 :: forall a. [a] -> [a]
  f2 = \(x:xs) -> xs ++ [ x :: a ]   -- OK
  
  f3 :: forall a. [a] -> [a]
  Just f3 = Just (\(x:xs) -> xs ++ [ x :: a ])   -- Not OK!
  

  f1 — это связывание функции, а f2 связывает отдельную переменную; в обоих случаях сигнатура типа вводит a в область видимости. Однако связывание для f3 является связыванием образца, поэтому f3 — это новая переменная, вводимая в область видимости образцом и не связанная с переменной верхнего уровня f3. Следовательно, переменная типа a не находится в области видимости правой части Just f3 = ....

6.11.5.3. Сигнатуры типов выражений

Сигнатура типа выражения, содержащая явную квантификацию (с помощью forall), вводит явно квантифицированные переменные типа в область видимости аннотированного выражения. Например:

f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )

Здесь сигнатура типа forall s. ST s Bool вводит переменную типа s в область видимости аннотированного выражения (op >>= \(x :: STRef s Int) -> g x).

6.11.5.4. Сигнатуры типов в образцах

Сигнатура типа может встречаться в любом образце; это сигнатура типа в образце. Например:

-- f and g assume that 'a' is already in scope
f = \(x::Int, y::a) -> x

g (x::a) = x

h ((x,y) :: (Int,Bool)) = (y,x)

Если все переменные типа в сигнатуре типа в образце уже находятся в области видимости (то есть связаны во внешнем контексте), всё просто: сигнатура лишь накладывает очевидное ограничение на тип образца.

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

f :: forall a. [a] -> (Int, [a])
f xs = (n, zs)
  where
    (ys::[a], n) = (reverse xs, length xs) -- OK
    (zs::[a])    = xs ++ ys                     -- OK

    Just (v::b)  = ...  -- Not OK; b is not in scope

Здесь сигнатуры в образцах для ys и zs допустимы, а сигнатура для v — нет, поскольку b не находится в области видимости.

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

-- same f and g as above, now assuming that 'a' is not already in scope
f = \(x::Int, y::a) -> x           -- 'a' is in scope on RHS of ->

g (x::a) = x :: a

hh (Just (v :: b)) = v :: b

Сигнатура типа в образце делает переменную типа доступной в правой части уравнения.

Введение переменных типа в область видимости особенно важно для конструкторов данных с экзистенциальными типами. Например:

data T = forall a. MkT [a]

k :: T -> T
k (MkT [t::a]) =
    MkT t3
  where
    (t3::[a]) = [t,t,t]

Здесь сигнатура типа в образце [t::a] содержит лексическую переменную типа, которая ещё не находится в области видимости. Более того, она не должна там находиться, поскольку связывается сопоставлением с образцом. В результате эта переменная вводится в область видимости и обозначает переменную типа, связанную экзистенциально.

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

Сравните два (идентичных) определения для примеров f, g; оба допустимы независимо от того, находится ли a уже в области видимости. Разница в том, что, если a уже находится в области видимости, сигнатура накладывает ограничение на образец, а не связывает переменную в образце.

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

ScopedTypeVariables позволяет переменным типа, связанным в начале объявления class или instance, иметь область видимости в методах, определённых в части where. В отличие от сигнатур типов объявлений, переменные типа из объявлений классов и экземпляров могут иметь лексическую область видимости без явного forall (хотя в объявлении instance допускается явный forall; см. явную универсальную квантификацию (forall)). Например:

class C a where
  op :: [a] -> a

  op xs = let ys::[a]
              ys = reverse xs
          in
          head ys

instance C b => C [b] where
  op xs = reverse (head (xs :: [[b]]))

-- Alternatively, one could write the instance above as:
instance forall b. C b => C [b] where
  op xs = reverse (head (xs :: [[b]]))

Хотя для того, чтобы переменные типа из начала объявления класса или экземпляра распространялись на /тела/ методов, требуется ScopedTypeVariables, для распространения переменных типа на /сигнатуры типов/ методов это расширение не требуется. Например, следующий код будет принят без явного включения ScopedTypeVariables:

class D a where
  m :: a -> a

instance Num a => D [a] where
  m :: [a] -> [a]
  m x = map (*2) x

Обратите внимание, что для записи m :: [a] -> [a] требуется расширение InstanceSigs.

Аналогично, ScopedTypeVariables не требуется, чтобы переменные типа из начала объявления класса или экземпляра распространялись на связанные семейства типов; для этого достаточно расширения TypeFamilies. Например, следующий код будет принят без явного включения ScopedTypeVariables:

class E a where
  type T a

instance E [a] where
  type T [a] = a

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