6.4.19. Обязательные аргументы типа

6.4.19.1. Терминология: зависимый квантор

И forall a., и forall a -> называют «зависимыми», поскольку результирующий тип зависит от переданного аргумента типа:

id @Integer :: Integer -> Integer
id @String  :: String  -> String

id_vdq Integer :: Integer -> Integer
id_vdq String  :: String  -> String

Обратите внимание, как правая часть сигнатуры зависит от левой.

Это отличается от стрелки функции ->, которая является независимым квантором:

putStrLn "Hello" :: IO ()
putStrLn "World" :: IO ()

Тип putStrLn — String -> IO (). Какую бы строку мы ни передали на вход, результирующий тип IO () от неё не зависит.

Это понятие зависимости слабее понятия, используемого в языках с зависимой типизацией (см. Связь с Π-типами).

6.4.19.2. Терминология: видимый квантор

Мы называем forall a. невидимым квантором, а forall a -> — видимым. Это понятие «видимости» не связано с неявной квантификацией, которая происходит, когда квантор опущен:

id     ::             a -> a    -- implicit quantification, invisible forall
id     :: forall a.   a -> a    -- explicit quantification, invisible forall
id_vdq :: forall a -> a -> a    -- explicit quantification,   visible forall

Свойство «видимости» описывает, виден ли соответствующий аргумент типа в месте определения и в местах вызова:

-- Invisible quantification
id :: forall a. a -> a
id x = x                -- defn site: `a` is not mentioned
call_id = id True       -- call site: `a` is invisibly instantiated to `Bool`

-- Visible quantification
id_vdq :: forall a -> a -> a
id_vdq t x = x                  -- defn site: `a` is visibly bound to `t`
call_id_vdq = id_vdq Bool True  -- call site: `a` is visibly instantiated to `Bool`

В уравнении для id слева находится лишь один связыватель — x; он соответствует аргументу-значению, а не аргументу типа. Сравните это с определением id_vdq:

id_vdq :: forall a -> a -> a
id_vdq t x = x

На этот раз слева у нас два связывателя:

• t, соответствующий forall a -> в сигнатуре
• x, соответствующий a -> в сигнатуре

Связанную переменную t можно использовать в последующих шаблонах, а также в правой части уравнения:

id_vdq :: forall a -> a -> a
id_vdq t (x :: t) = x :: t
--     ↑       ↑         ↑
--   bound    used      used

Термины «видимый аргумент типа» и «обязательный аргумент типа» используются как синонимы.

6.4.19.3. Связь с TypeApplications

RequiredTypeArguments похожи на TypeApplications: в обоих случаях мы передаём функции тип как явный аргумент. Разница в том, что применение типов необязательно: вызывающий код сам решает, написать ли id @Bool True или id True. По умолчанию компилятор выводит, что переменная типа инстанцируется в Bool. Наличие аргумента типа синтаксически не отражается в выражении: он невидим, если не использовать переопределение видимости, то есть @.

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

x1 = id_vdq Bool True    -- OK
x2 = id_vdq      True    -- not OK

Для вывода обязательного аргумента типа можно использовать подчёркивание:

x3 = id_vdq _ True       -- OK

Таким образом, выбор между forall a. с применением типов и forall a -> — в основном вопрос синтаксиса. Одно из преимуществ обязательных аргументов типа состоит в том, что они никогда не бывают неоднозначными. Рассмотрим тип Foreign.Storable.sizeOf:

sizeOf :: forall a. Storable a => a -> Int

Параметр-значение на самом деле не используется; он нужен лишь для управления выводом типов. В местах вызова можно написать sizeOf (undefined :: Bool) или sizeOf @Bool undefined. В любом случае undefined совершенно избыточен и существует только для того, чтобы избежать неоднозначной переменной типа.

С помощью RequiredTypeArguments можно представить немного другой API:

sizeOf :: forall a -> Storable a => Int

Если бы sizeOf имел такой тип, можно было бы написать sizeOf Bool, не передавая фиктивное значение.

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

6.4.19.4. Связь с ExplicitNamespaces

Обязательный аргумент типа синтаксически неотличим от аргумента-значения. В вызове функции f arg1 arg2 arg3 невозможно определить, не зная тип f, какие из трёх аргументов являются обязательными аргументами типа, если такие есть.

При этом одна из целей разработки GHC — обеспечить разрешение имён (поиск мест связывания идентификаторов) без привлечения системы типов. Рассмотрим:

data Ty = Int | Double | String deriving Show
main = print Int

В этом примере в области видимости есть два конструктора с именем Int:

• конструктор типа Int рода Type (импортирован из Prelude)
• конструктор данных Int типа Ty (определён локально)

Как компилятор или читатель кода узнаёт, что print Int должно ссылаться на конструктор данных, а не на конструктор типа? В GHC это решается следующим образом. Считается, что каждый идентификатор встречается либо в синтаксисе типов, либо в синтаксисе термов — в зависимости от окружающего синтаксического контекста:

-- Examples of X in type syntax
type T = X      -- RHS of a type synonym
data D = MkD X  -- field of a data constructor declaration
a :: X          -- RHS of a type signature
b = f (c :: X)  -- RHS of a type signature (in expressions)
f (x :: X) = x  -- RHS of a type signature (in patterns)

-- Examples of X in term syntax
c X = a         -- LHS of a function equation
c a = X         -- RHS of a function equation

Можно представить, что вся программа «разделена на зоны» синтаксиса типов и синтаксиса термов, причём в каждой зоне действуют собственные правила разрешения имён:

• В синтаксисе типов приоритет имеют конструкторы типов.
• В синтаксисе термов приоритет имеют конструкторы данных.

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

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

vshow :: forall a -> Show a => a -> String
vshow t x = show (x :: t)

s1 = vshow Int    42      -- "42"
s2 = vshow Double 42      -- "42.0"

Вызовы функций vshow Int 42 и vshow Double 42 записаны в синтаксисе термов, тогда как предполагаемые объекты ссылок Int и Double — соответствующие конструкторы типов. Пока в области видимости нет конструкторов данных с именами Int или Double, пример работает как задумано. Однако если ввести конфликтующие имена конструкторов, это может нарушить разрешение имён:

data Ty = Int | Double | String

vshow :: forall a -> Show a => a -> String
vshow t x = show (x :: t)

s1 = vshow Int    42      -- error: Expected a type, but ‘Int’ has kind ‘Ty’
s2 = vshow Double 42      -- error: Expected a type, but ‘Double’ has kind ‘Ty’

В этом примере предполагалось использовать Int и Double как типы, но имена были разрешены в пользу конструкторов данных, что привело к ошибкам типов.

Исправить пример можно с помощью ExplicitNamespaces, которое позволяет встраивать синтаксис типов в синтаксис термов с помощью ключевого слова type:

s1 = vshow (type Int)    42
s2 = vshow (type Double) 42

Похожая проблема возникает с синтаксисом списков и кортежей. В синтаксисе типов [a] обозначает тип списка, то есть Data.List.List a. В синтаксисе термов [a] — это список из одного элемента, то есть a : []. Наивная попытка использовать тип списка в качестве обязательного аргумента типа приведёт к ошибке типов:

s3 = vshow [Int] [1,2,3]  -- error: Expected a type, but ‘[Int]’ has kind ‘[Type]’

Проблема в том, что GHC считает, что [Int] обозначает Int : [], а не предполагаемый Data.List.List Int. Это тоже можно исправить с помощью ключевого слова type:

s3 = vshow (type [Int]) [1,2,3]

Поскольку ключевое слово type служит лишь для устранения неоднозначности пространств имён, его не обязательно применять ко всему аргументу типа. Допустимо использовать его и только для устранения неоднозначности части аргумента типа:

f :: forall a -> ...   -- `f`` is a function that expects a required type argument

r1 = f (type (Either () Int))           -- `type` applied to the entire type argument
r2 = f (Either (type ()) Int)           -- `type` applied to one part of it
r3 = f (Either (type ()) (type Int))    -- `type` applied to multiple parts

Иными словами, выражение Either (type ()) (type Int) не означает, что к Either применяются два аргумента типа; напротив, всё выражение является одним аргументом типа, а type используется для устранения неоднозначности отдельных его частей.

За пределами обязательного аргумента типа использовать type запрещено:

r4 = type Int  -- illegal use of ‘type’

6.4.19.5. Типы в термах

Начиная с: GHC 9.12

Расширение RequiredTypeArguments дополняет грамматику выражений уровня термов синтаксисом, обычно встречающимся только в типах:

• типы функций: a -> b, a ⊸ b, a %m -> b
• типы с ограничениями: ctx => t
• типы с всеобщими кванторами: forall tvs. t, forall tvs -> t

Так называемые «типы в термах» позволяют передавать любые типы в качестве обязательных аргументов типа:

a1 = f (Int -> Bool)                       -- function type
a2 = f (Int %1 -> String)                  -- linear function type
a3 = f (Read T => T)                       -- constrained type
a4 = f (forall a. a)                       -- universally quantified type
a5 = f (forall a. Read a => String -> a)   -- a combination of the above

Есть несколько ограничений:

• Синтаксис * из StarIsType недоступен из-за конфликта с оператором умножения. Вместо него используйте Type из модуля Data.Kind.
• Синтаксис ' из DataKinds недоступен из-за конфликта с кавычками имён из TemplateHaskell. Вместо этого просто опустите '.

6.4.19.6. Влияние на неявную квантификацию

Неявная квантификация происходит, когда GHC добавляет неявный forall для связывания переменных типа:

const :: a -> b -> a               -- implicit quantification
const :: forall a b. a -> b -> a   -- explicit quantification

Обычно неявная квантификация не зависит от переменных термов в области видимости:

f a = ...  -- the LHS binds `a`
  where const :: a -> b -> a
           -- implicit quantification over `a` takes place
           -- despite the `a` bound on the LHS of `f`

Когда включено расширение RequiredTypeArguments, имена, связанные в синтаксисе термов, не квантифицируются неявно. Это позволяет принять следующий пример:

readshow :: forall a -> (Read a, Show a) => String -> String
readshow t s = show (read s :: t)

s1 = readshow Int    "42"      -- "42"
s2 = readshow Double "42"      -- "42.0"

Обратите внимание: t связано в левой части уравнения функции (синтаксис термов), а затем используется в аннотации типа (синтаксис типов). Согласно обычным правилам неявной квантификации, t квантифицировалось бы неявно:

-- RequiredTypeArguments
readshow t s = show (read s :: t)   -- the `t` is captured
--       ↑                     ↑
--      bound                 used

-- NoRequiredTypeArguments
readshow t s = show (read s :: t)   -- the `t` is implicitly quantified as follows:
readshow t s = show (read s :: forall t. t)
--       ↑                            ↑  ↑
--      bound                      bound used

С одной стороны, учёт текущей области видимости позволяет принимать программы вроде приведённой выше. С другой стороны, некоторые существующие программы перестанут компилироваться:

a = 42
f :: a -> a    -- RequiredTypeArguments: the top-level `a` is captured

Поэтому одно лишь включение расширения RequiredTypeArguments может привести к ошибкам типов такого вида:

Term variable ‘a’ cannot be used here
  (term variables cannot be promoted)

Есть два способа исправить эту ошибку:

a = 42
f1 :: b -> b              -- (1) use a different variable name
f2 :: forall a. a -> a    -- (2) use an explicit forall

Если вы адаптируете большую кодовую базу для совместимости с RequiredTypeArguments, рассмотрите возможность использовать -Wterm-variable-capture на время миграции. Это предупреждение обнаруживает случаи неявной квантификации, несовместимые с RequiredTypeArguments:

The type variable ‘a’ is implicitly quantified,
even though another variable of the same name is in scope:
  ‘a’ defined at ...

6.4.19.7. Связь с Π-типами

И forall a., и forall a -> являются зависимыми кванторами в узком смысле, определённом в разделе Терминология: зависимый квантор. Однако ни один из них не образует зависимый тип функции (Π-тип), знакомый пользователям языков с зависимой типизацией или систем доказательств.

• В Haskell всегда были функции, результативное значение которых зависит от значения аргумента:

  not True  = False   -- argument value: True;  result value: False
  (*2) 5    = 10      -- argument value: 5;     result value: 10
  

  Это соответствует обычному понятию функции, обозначаемой a -> b.

• В Haskell также есть функции, результирующий тип которых зависит от типа аргумента:

  id    @Int  :: Int  -> Int    -- argument type: Int;  result type: Int  -> Int
  id_vdq Bool :: Bool -> Bool   -- argument type: Bool; result type: Bool -> Bool
  

  Это соответствует понятию параметрического полиморфизма, обозначаемого forall a. b или forall a -> b.

• Кроме того, в Haskell есть функции, результативное значение которых зависит от типа аргумента:

  maxBound @Int8   = 127    -- argument type: Int8;  result value: 127
  maxBound @Int16  = 32767  -- argument type: Int16; result value: 32767
  

  Это соответствует понятию ad hoc-полиморфизма (полиморфизма на основе классов), обозначаемого C a => b.

• Однако Haskell не поддерживает напрямую функции, результирующий тип которых зависит от значения аргумента. В литературе их часто называют «зависимыми функциями» или «Π-типами».

  Рассмотрим:

  type F :: Bool -> Bool
  type family F b where
    F True  = ...
    F False = ...
  
  f :: Bool -> Bool
  f True  = ...
  f False = ...
  

  В этом примере мы определяем семейство типов F, сопоставляющее с образцом b на уровне типов, и функцию f, сопоставляющую с образцом b на уровне термов. Однако невозможно квантифицировать b так, чтобы к нему можно было применить и F, и f:

  depfun :: forall (b :: Bool) -> F b  -- Allowed
  depfun b = ... (f b) ...             -- Not allowed
  

  Передавать b в f запрещено, потому что b не существует во время выполнения. Типы и аргументы типов удаляются до выполнения программы.

Расширение RequiredTypeArguments не добавляет зависимые функции — это было бы гораздо более серьёзным шагом. Расширение RequiredTypeArguments лишь позволяет сделать аргументы типа функции обязательными.

6.4.19.8. Видимый forall в GADT

Начиная с: GHC 9.14

При включённом расширении RequiredTypeArguments разрешается использовать forall a -> в объявлениях конструкторов данных:

data T a where
  Typed :: forall a -> a -> T a

Ограничений на вид родительского объявления нет: конструктор данных может быть введён в составе объявления data, data instance, newtype или newtype instance.

Использование видимого forall в типе конструктора данных не ограничивает места, где может встречаться этот конструктор. Например:

• в выражениях

  t1 = Typed Int 42
  t2 = Typed String "hello"
  t3 = Typed (Int -> Bool) even
  

• в шаблонах

  f1 (Typed a x) = x :: a
  f2 (Typed Int n) = n*2
  f3 (Typed ((->) w Bool) g) = not . g
  

• в типах (с DataKinds)

  type T1 = Typed Nat 42
  type T2 = Typed Symbol "hello"
  type T3 = Typed (Type -> Constraint) Num
  

В настоящее время все forall в типе конструктора данных (в том числе видимые forall) должны располагаться перед ограничениями или аргументами-значениями:

data D x where
  -- OK (one forall at the front of the type)
  MkD1 :: forall a b ->
          a ->
          b ->
          D (a, b)

  -- OK (multpile foralls at the front of the type)
  MkD2 :: forall a.
          forall b ->
          a ->
          b ->
          D (a, b)

  -- Rejected (forall after a value argument)
  MkD3 :: forall a ->
          a ->
          forall b ->
          b ->
          D (a, b)

В будущем это ограничение планируется снять (#18389).

Использование видимого forall вместо невидимого никак не влияет на представление данных в куче.