6.4.16. Применение видимого типа

6.4.16.1. Выводные и заданные переменные типа

GHC отслеживает различие между переменными типа, которые мы называем выведенными и заданными. Только заданные переменные типа доступны для подстановки при видимом применении типов. Пример хорошо это иллюстрирует:

f :: (Eq b, Eq a) => a -> b -> Bool
f x y = (x == x) && (y == y)

g x y = (x == x) && (y == y)

Функции f и g имеют одинаковое тело, но только f имеет сигнатуру типа. Когда GHC вычисляет, как обработать видимое применение типа, он должен знать, какую переменную подставить. Поэтому он должен иметь возможность задать порядок переменных типа в типе функции.

Если пользователь предоставил сигнатуру типа, как в f, то это легко: мы просто берём порядок из сигнатуры типа, слева направо и используем первое вхождение переменной для выбора её позиции в порядке. Таким образом, переменные в f будут b, затем a.

В отличие от этого, для g нет надёжного способа сделать это; мы не будем знать, Eq a или Eq b будут указаны первыми в ограничении в типе g. Для того, чтобы видимое применение типов было надёжным между выпусками GHC, мы запрещаем его использование с g.

Мы говорим, что переменные типа в f являются заданными, а те в g — выведенными. Общее правило таково: если пользователь написал переменную типа в исходной программе, она является заданной; если нет, она является выведенной.

Это правило применяется и к объявлениям типов данных. Например, если у нас есть data Proxy a = Proxy (и PolyKinds включено), то a будет присвоено родовое значение k, где k — новая переменная рода. Поскольку k не был написан пользователем, он будет недоступен для применения типа в типе конструктора Proxy; доступны только a.

Выводные переменные печатаются в фигурных скобках. Таким образом, тип конструктора данных Proxy из предыдущего примера — forall {k} (a :: k). Proxy a. Мы можем наблюдать это поведение в сеансе GHCi:

> :set -XTypeApplications -fprint-explicit-foralls
> let myLength1 :: Foldable f => f a -> Int; myLength1 = length
> :type myLength1
myLength1 :: forall (f :: * -> *) a. Foldable f => f a -> Int
> let myLength2 = length
> :type myLength2
myLength2 :: forall {t :: * -> *} {a}. Foldable t => t a -> Int
> :type myLength2 @[]

<interactive>:1:1: error:
    • Cannot apply expression of type ‘t0 a0 -> Int’
      to a visible type argument ‘[]’
    • In the expression: myLength2 @[]

Обратите внимание, что поскольку myLength1 был определён с явной сигнатурой типа, :type сообщает, что все его переменные типа доступны для применения типа. С другой стороны, myLength2 не имела сигнатуры типа. В результате все его переменные типа окружены фигурными скобками, и попытка использовать видимое применение типа с myLength2 терпит неудачу.

6.4.16.2. Порядок заданных переменных

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

• Если тип идентификатора имеет forall, то порядок переменных типа, как написано в forall, сохраняется.

• Если какие-либо из переменных зависят от других переменных (то есть, если некоторые из переменных являются родовыми переменными), переменные переупорядочиваются так, что родовые переменные предшествуют переменным типа, сохраняя порядок слева направо насколько это возможно. То есть GHC выполняет устойчивую топологическую сортировку переменных. Пример:

  h :: Proxy (a :: (j, k)) -> Proxy (b :: Proxy a) -> ()
    -- as if h :: forall j k a b. ...
  

  В этом примере a зависит от j и k, а b зависит от a. Несмотря на то, что a лексически предшествует j и k, j и k квантифицируются первыми, потому что a зависит от j и k. Кроме того, обратите внимание, что j и k не переупорядочиваются друг относительно друга, даже если это не нарушит зависимостей.

  Здесь «устойчивая топологическая сортировка» означает, что мы выполняем этот алгоритм (который мы называем ScopedSort):

  • Обрабатываем входной список переменных типа слева направо с курсором.
  • Если переменная v в курсоре зависит от какой-либо предыдущей переменной w, переместить v сразу перед самой левой такой w.
• Аргументы типа методов класса включают переменные типа класса, за которыми следуют любые переменные, в которых метод является полиморфным. Таким образом, class Monad m where return :: a -> m a означает, что аргументы типа return — m, a.
• С помощью расширения RankNTypes (Лексически-определённые переменные типа) можно объявлять аргументы типа не в начале типа. Например, мы можем иметь pair :: forall a. a -> forall b. b -> (a, b) и затем сказать pair @Bool True @Char, что будет иметь тип Char -> (Bool, Char).
• Частичные сигнатуры типов (Частичные сигнатуры типов) хорошо работают с видимым применением типов. Если вы хотите указать только второй аргумент типа для wurble, тогда вы можете сказать wurble @_ @Int. Первый аргумент является подстановочным, как и в частичной сигнатуре типа. Однако, если используется видимое применение типа/видимое применение рода, не нужно указывать PartialTypeSignatures, и ваш код не сгенерирует предупреждение, сообщающее об опущенном типе.

Раздел этой справки по полиморфизму рода описывает, как упорядочиваются переменные в объявлениях типов и классов (Вывод порядка переменных в объявлении типа/класса).

6.4.16.3. Ручное определение выводимых переменных

С выпуска 9.0.1 GHC позволяет помечать переменные типов или видов, написанные пользователем, как выводимые, в отличие от значения по умолчанию — указанные. Написав связующую переменную типа в фигурных скобках, как {tyvar} или {tyvar :: kind}, новая переменная будет классифицирована как выводимая, а не указанная. Это дает программисту контроль над тем, какие переменные можно вручную инициализировать, а какие нет. Обратите внимание, что фигурные скобки не влияют на область видимости: переменные в фигурных скобках все равно входят в область видимости. Рассмотрим, например:

myConst :: forall {a} b. a -> b -> a
myConst x _ = x

В этом примере, несмотря на то, что обе переменные появляются в сигнатуре типа, a является выводимой переменной, а b — указанной. Это означает, что выражение myConst @Int имеет тип forall {a}. a -> Int -> a.

Фигурные скобки разрешены в следующих местах:

• В сигнатурах типов функций, переменных, методов класса, а также аннотациях типов выражений. Рассмотрите пример выше.

• В объявлениях конструкторов данных, используя синтаксис GADT. Рассмотрим:

  data T a where MkT :: forall {k} (a :: k). Proxy a -> T a
  

  Конструктор MkT , определённый в этом примере, является полиморфным по виду, что подчеркивается для читателя путём явного абстрагирования от переменной k. Поскольку эта переменная помечена как выводимая, её нельзя вручную инициализировать.

• В квантификациях переменных существования, например:

  data HList = HNil
             | forall {a}. HCons a HList
  

• В сигнатурах синонимов шаблонов. Например:

  data T a where MkT :: forall a b. a -> b -> T a
  
  pattern Pat :: forall {c}. () => forall {d}. c -> d -> T c
  pattern Pat x y = MkT x y
  

  Обратите внимание, что в этом примере a является универсальной переменной в типе данных T, где b является экзистенциальной. При написании синонима шаблона оба типа могут быть указанными или выводимыми.

• В правой части синонима типа, например:

  type Foo = forall a {b}. Either a b
  

• В сигнатурах типов переменных, связанных в RULES, например:

  {-# RULES "parametricity" forall (f :: forall {a}. a -> a). map f = id #-}
  

Фигурные скобки не разрешены в следующих местах:

• В видимых зависимых квантификаторах. Рассмотрим:

  data T :: forall {k} -> k -> Type
  

  Этот пример отклоняется, поскольку видимый аргумент по определению должен быть явно применён. Сделать их выводимыми (и, следовательно, неприменимыми) противоречило бы этому.

• В предикатах SPECIALISE или в заголовках объявлений экземпляров, например:

  instance forall {a}. Eq (Maybe a) where ...
  

  Причина этого заключается в том, что ни одно из них не определяет новую конструкцию. Это означает, что ни один новый тип не определяется, где специфичность могла бы играть роль.

• В левой части объявлений типов, таких как классы, типы данных и т. д.

Обратите внимание, что хотя указанные и выводимые переменные типов обладают различными свойствами по отношению к видимому применению типов, они не влияют иначе на понятие равенства типов в GHC. Например, при заданных определениях:

id1 :: forall a. a -> a
id1 x = x

id2 :: forall {a}. a -> a
id2 x = x

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

app2 :: (forall {a}. a -> a) -> b -> b
app2 g x = g x

GHC сочтёт все app1 id1, app1 id2, app2 id1, и app2 id2 хорошо типизированными.