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», поэтому «x::a» означает «x::forall a. a» в соответствии с обычными правилами неявного квантования Haskell.

• Переменная типа квантуется единственной, синтаксически видимой, внешней 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 (хотя вы можете использовать явный forall в объявлении instance ; см. Явное универсальное квантификация (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

См. Ограничение параметров класса для получения дополнительной информации.