6.4.17. 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

Note that 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 essence of a forall is the same regardless of whether it is followed by a dot or an arrow: it introduces a type variable. But the way we bind and specify this type variable at the term level differs.

When we define id, we can use a lambda to bind a variable that stands for the function argument:

-- For reference: id :: forall a. a -> a
id = \x -> x

At the same time, there is no mention of a in this definition at all. It is bound by the compiler behind the scenes, and that is why we call the ordinary forall a. an invisible quantifier. Compare that to forall a ->, which is considered visible:

-- For reference: id_vdq :: forall a -> a -> a
id_vdq = \(type t) x -> x

This time we have two binders in the lambda: * type t, corresponding to forall a -> in the signature * x, corresponding to a -> in the signature

And of course, now we also have the option of using the bound t in a subsequent pattern, as well as on the right-hand side of the lambda:

-- For reference: id_vdq :: forall a -> a -> a
id_vdq = \(type t) (x :: t) -> x :: t
--              ↑        ↑          ↑
--            bound     used       used

At use sites, we also instantiate this type variable explicitly:

n = id_vdq (type Integer) 42
s = id_vdq (type String)  "Hello"

6.4.17.1. 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 (type Bool) True    -- OK
x2 = id_vdq             True    -- not OK

You may use an underscore to infer a required type argument:

x3 = id_vdq (type _) 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 (type Bool) without passing a dummy value.

6.4.17.2. Relation to ExplicitNamespaces

The type keyword that we used in the examples is not actually part of RequiredTypeArguments. It is guarded behind ExplicitNamespaces. As described in the proposal, required type arguments can be passed without a syntactic marker, making them syntactically indistinguishble from ordinary function arguments:

n = id_vdq Integer 42

In this example we pass Integer as opposed to (type Integer). This is not currently implemented, but it demonstrates how RequiredTypeArguments is not tied to the type syntax. For this reason, using the type syntax requires enabling the ExplicitNamespaces extension separately.