Type-level type applications¶
Allow the use of type applications at the type level. For example, we could write:
'Just @Nat
instead of:
'Just :: Nat -> Maybe Nat
Motivation¶
There are two major motivations:
To allow users to get the power and convenience of explicit type applications at the type level as well as the term level.
To allow
-fprint-explicit-kinds
and theShow
instance forTypeRep
to produce more readable output. Currently,show (typeRep @('Just 3))
produces"'Just Nat 3"
, making no distinction between levels. With the proposed change, we could quite legitimately produce"'Just @Nat 3"
, which seems much clearer.
Proposed Change Specification¶
Allow visible type application in types as well as terms. In precisely
the same way that it currently is used to reduce forall
s in terms,
it will reduce forall
s in types. This new behavior will be controlled
by the -XTypeApplications
extension.
Specifically:
Add new parsing rules to types allowing
@
to appear before a type argument.Currently, GHC tracks three visibilities: required, specified, and inferred. A required argument must be applied at every call site. These are normal arguments, like the
a
argument toMaybe a
. Specified arguments are arguments that are normally omitted but can be supplied explicitly with the use of@
. For example, thek
indata Proxy :: forall k. k -> Type
is specified. Inferred arguments are not available for explicit application, like the kind ofa
indata Proxy2 a
.With visible type application in types, users could provide explicit instantiations of specified arguments.
In an extension to existing rules, a variable must be mentioned somewhere in the Haskell source to be specified. A variable that is never written in the source is inferred.
Promoted data constructor arguments have the same visibilities as the unpromoted data constructor.
GHC’s current behavior of implicitly quantifying over type variables used in type signatures is unaffected. If a type variable is mentioned only in a visible type application, it is still implicitly quantified.
Effect and Interactions¶
This new feature would work in pattern signatures (that is, a type signature ascribing a type to a term-level pattern) and would have the capability of binding a scoped type variable. Viz:
data Ex where
MkEx :: forall k (a :: k). Proxy (a :: k) -> Ex
foo (MkEx (p :: Proxy @k a)) = ... k is in scope here (along with a) ...
Costs and Drawbacks¶
As a user, I was quite surprised to find that this didn’t work already, so I don’t think the learning cost will be high.
The development costs should be relatively low. Instantiation in types is already lazy, and so type application in types will be much easier to implement than type application in terms was.
Alternatives¶
I am not aware of any existing alternatives.
Unresolved questions¶
Should we change the behavior of :kind
to match that of :type
? Currently, the latter
does instantiation while the former does not. This means that there is no screaming need
to introduce a :kind +v
, because :kind
is already analogous to :type +v
. Perhaps
this is confusing though.
Implementation Plan¶
Richard Eisenberg (@goldfirere) is happy to advise someone who wants to take this on. Or he will implement himself someday.