6.4.18. Требуемые типы аргументов

6.4.18.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.18.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.18.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.18.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.18.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.18.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.18.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
  

  Это захватывает идею ад-хок (основанного на классах) полиморфизма, обозначаемого 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 просто делает возможным обязательным указание аргументов типа функции.