6.4.18. Required type arguments¶

RequiredTypeArguments
¶ Since: 9.10.1 Status: Experimental Allow visible dependent quantification
forall x >
in types of terms.
This feature is only partially implemented in GHC. In this section we describe the implemented subset, while the full specification can be found in GHC Proposal #281.
The RequiredTypeArguments
extension enables the use of visible
dependent quantification in types of terms:
id :: forall a. a > a  invisible dependent quantification
id_vdq :: forall a > a > a  visible dependent quantification
The arrow in forall a >
is part of the syntax and not a function arrow,
just like the dot in forall a.
is not a type operator.
The choice between forall a.
and forall a >
does not have any effect on
program execution. Both quantifiers introduce type variables, which are erased
during compilation. Rather, the main difference is in the syntax used at call
sites:
x1 = id True  invisible forall, the type argument is inferred by GHC
x2 = id @Bool True  invisible forall, the type argument is supplied by the programmer
x3 = id_vdq _ True  visible forall, the type argument is inferred by GHC
x4 = id_vdq Bool True  visible forall, the type argument is supplied by the programmer
6.4.18.1. Terminology: Dependent quantifier¶
Both forall a.
and forall a >
are said to be “dependent” because the
result type depends on the supplied type argument:
id @Integer :: Integer > Integer
id @String :: String > String
id_vdq Integer :: Integer > Integer
id_vdq String :: String > String
Notice how the RHS of the signature is influenced by the LHS.
This is in contrast to the function arrow >
, which is a nondependent
quantifier:
putStrLn "Hello" :: IO ()
putStrLn "World" :: IO ()
The type of putStrLn
is String > IO ()
. No matter what string we pass
as input, the result type IO ()
does not depend on it.
This notion of dependence is weaker than the one used in dependentlytyped languages (see Relation to Πtypes).
6.4.18.2. Terminology: Visible quantifier¶
We say that forall a.
is an invisible quantifier and forall a >
is a
visible quantifier. This notion of “visibility” is unrelated to implicit
quantification, which happens when the quantifier is omitted:
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
The property of “visibility” actually describes whether the corresponding type argument is visible at the definition site and at call sites:
 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`
In the equation for id
there is just one binder on the LHS, x
, and it
corresponds to the value argument, not to the type argument. Compare that with
the definition of id_vdq
:
id_vdq :: forall a > a > a
id_vdq t x = x
This time we have two binders on the LHS:
t
, corresponding toforall a >
in the signaturex
, corresponding toa >
in the signature
The bound t
can be used in subsequent patterns, as well as on the righthand
side of the equation:
id_vdq :: forall a > a > a
id_vdq t (x :: t) = x :: t
 ↑ ↑ ↑
 bound used used
We use the terms “visible type argument” and “required type argument” interchangeably.
6.4.18.3. Relation to TypeApplications
¶
RequiredTypeArguments
are similar to TypeApplications
in that we pass a type to a function as an explicit argument. The difference is
that type applications are optional: it is up to the caller whether to write
id @Bool True
or id True
. By default, the compiler infers that the
type variable is instantiated to Bool
. The existence of a type argument is
not reflected syntactically in the expression, it is invisible unless we use a
visibility override, i.e. @
.
Required type arguments are compulsory. They must appear syntactically at call sites:
x1 = id_vdq Bool True  OK
x2 = id_vdq True  not OK
You may use an underscore to infer a required type argument:
x3 = id_vdq _ True  OK
That is, it is mostly a matter of syntax whether to use forall a.
with type
applications or forall a >
. One advantage of required type arguments is that
they are never ambiguous. Consider the type of Foreign.Storable.sizeOf
:
sizeOf :: forall a. Storable a => a > Int
The value parameter is not actually used, its only purpose is to drive type
inference. At call sites, one might write sizeOf (undefined :: Bool)
or
sizeOf @Bool undefined
. Either way, the undefined
is entirely
superfluous and exists only to avoid an ambiguous type variable.
With RequiredTypeArguments
, we can imagine a slightly different API:
sizeOf :: forall a > Storable a => Int
If sizeOf
had this type, we could write sizeOf Bool
without
passing a dummy value.
Required type arguments are erased during compilation. While the source program appears to bind and pass required type arguments alongside value arguments, the compiled program does not. There is no runtime overhead associated with required type arguments relative to the usual, invisible type arguments.
6.4.18.4. Relation to ExplicitNamespaces
¶
A required type argument is syntactically indistinguishable from a value
argument. In a function call f arg1 arg2 arg3
, it is impossible to tell,
without looking at the type of f
, which of the three arguments are required
type arguments, if any.
At the same time, one of the design goals of GHC is to be able to perform name resolution (find the binding sites of identifiers) without involving the type system. Consider:
data Ty = Int  Double  String deriving Show
main = print Int
In this example, there are two constructors named Int
in scope:
 The type constructor
Int
of kindType
(imported fromPrelude
)  The data constructor
Int
of typeTy
(defined locally)
How does the compiler or someone reading the code know that print Int
is
supposed to refer to the data constructor, not the type constructor? In GHC,
this is resolved as follows. Each identifier is said to occur either in
type syntax or term syntax, depending on the surrounding syntactic
context:
 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
One could imagine the entire program “zoned” into type syntax and term syntax, each zone having its own rules for name resolution:
 In type syntax, type constructors take precedence over data constructors.
 In term syntax, data constructors take precedence over type constructors.
This means that in the print Int
example, the data constructor is selected
solely based on the fact that the Int
occurs in term syntax. This is firmly
determined before GHC attempts to typecheck the expression, so the type of
print
does not influence which of the two Int
s is passed to it.
This may not be the desired behavior in a required type argument. Consider:
vshow :: forall a > Show a => a > String
vshow t x = show (x :: t)
s1 = vshow Int 42  "42"
s2 = vshow Double 42  "42.0"
The function calls vshow Int 42
and vshow Double 42
are written in
term syntax, while the intended referents of Int
and Double
are the
respective type constructors. As long as there are no data constructors named
Int
or Double
in scope, the example works as intended. However, if such
clashing constructor names are introduced, they may disrupt name resolution:
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’
In this example the intent was to refer to Int
and Double
as types, but
the names were resolved in favor of data constructors, resulting in type errors.
The example can be fixed with the help of ExplicitNamespaces
, which
allows embedding type syntax into term syntax using the type
keyword:
s1 = vshow (type Int) 42
s2 = vshow (type Double) 42
A similar problem occurs with list and tuple syntax. In type syntax, [a]
is
the type of a list, i.e. Data.List.List a
. In term syntax, [a]
is a
singleton list, i.e. a : []
. A naive attempt to use the list type as a
required type argument will result in a type error:
s3 = vshow [Int] [1,2,3]  error: Expected a type, but ‘[Int]’ has kind ‘[Type]’
The problem is that GHC assumes [Int]
to stand for Int : []
instead of
the intended Data.List.List Int
. This, too, can be solved using the type
keyword:
s3 = vshow (type [Int]) [1,2,3]
Since the type
keyword is merely a namespace disambiguation mechanism, it
need not apply to the entire type argument. Using it to disambiguate only a part
of the type argument is also valid:
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
That is, the expression Either (type ()) (type Int)
does not indicate that
Either
is applied to two type arguments; rather, the entire expression is a
single type argument and type
is used to disambiguate parts of it.
Outside a required type argument, it is illegal to use type
:
r4 = type Int  illegal use of ‘type’
Finally, there are types that require the type
keyword only due to
limitations of the current implementation:
a1 = f (type (Int > Bool))  function type
a2 = f (type (Read T => T))  constrained type
a3 = f (type (forall a. a))  universally quantified type
a4 = f (type (forall a. Read a => String > a))  a combination of the above
This restriction will be relaxed in a future release of GHC.
6.4.18.5. Effect on implicit quantification¶
Implicit quantification is said to occur when GHC inserts an implicit forall
to bind type variables:
const :: a > b > a  implicit quantification
const :: forall a b. a > b > a  explicit quantification
Normally, implicit quantification is unaffected by term variables in scope:
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`
When RequiredTypeArguments
is in effect, names bound in term syntax
are not implicitly quantified. This allows us to accept the following example:
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"
Note how t
is bound on the LHS of a function equation (term syntax), and
then used in a type annotation (type syntax). Under the usual rules for implicit
quantification, the t
would have been implicitly quantified:
 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
On the one hand, taking the current scope into account allows us to accept programs like the one above. On the other hand, some existing programs will no longer compile:
a = 42
f :: a > a  RequiredTypeArguments: the toplevel `a` is captured
Because of that, merely enabling RequiredTypeArguments
might lead
to type errors of this form:
Term variable ‘a’ cannot be used here
(term variables cannot be promoted)
There are two possible ways to fix this error:
a = 42
f1 :: b > b  (1) use a different variable name
f2 :: forall a. a > a  (2) use an explicit forall
If you are converting a large codebase to be compatible with
RequiredTypeArguments
, consider using
Wtermvariablecapture
during the migration. It is a warning that
detects instances of implicit quantification incompatible with
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.6. Relation to Πtypes¶
Both forall a.
and forall a >
are dependent quantifiers in the narrow
sense defined in Terminology: Dependent quantifier. However, neither of them
constitutes a dependent function type (Πtype) that might be familiar to users
coming from dependentlytyped languages or proof assistants.
Haskell has always had functions whose result value depends on the argument value:
not True = False  argument value: True; result value: False (*2) 5 = 10  argument value: 5; result value: 10
This captures the usual idea of a function, denoted
a > b
.Haskell also has functions whose result type depends on the argument type:
id @Int :: Int > Int  argument type: Int; result type: Int > Int id_vdq Bool :: Bool > Bool  argument type: Bool; result type: Bool > Bool
This captures the idea of parametric polymorphism, denoted
forall a. b
orforall a > b
.Furthermore, Haskell has functions whose result value depends on the argument type:
maxBound @Int8 = 127  argument type: Int8; result value: 127 maxBound @Int16 = 32767  argument type: Int16; result value: 32767
This captures the idea of adhoc (classbased) polymorphism, denoted
C a => b
.However, Haskell does not have direct support for functions whose result type depends on the argument value. In the literature, these are often called “dependent functions”, or “Πtypes”.
Consider:
type F :: Bool > Bool type family F b where F True = ... F False = ... f :: Bool > Bool f True = ... f False = ...
In this example, we define a type family
F
to patternmatch onb
at the type level; and a functionf
to patternmatch onb
at the term level. However, it is impossible to quantify overb
in such a way that bothF
andf
could be applied to it:depfun :: forall (b :: Bool) > F b  Allowed depfun b = ... (f b) ...  Not allowed
It is illegal to pass
b
tof
becauseb
does not exist at runtime. Types and type arguments are erased before runtime.
The RequiredTypeArguments
extension does not add dependent
functions, which would be a much bigger step. Rather RequiredTypeArguments
just makes it possible for the type arguments of a function to be compulsory.