6.4.17. Видимое применение типа

6.4.17.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.17.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.17.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 — корректно типизированными.