Visible forall in types of terms, Part 2
GHC Proposal #281: Visible forall in types of terms is presented in two parts:
- Part 1 introduces the
forall a ->
quantifier in types of terms but also requires a syntactic marker at use sites. - Part 2 specifies when it is permissible to omit the
type
herald.
See also https://gitlab.haskell.org/ghc/ghc/-/wikis/DH-current-status.
The first part was tracked at #22326 (closed) and implemented in 33b6850a. This new ticket is to track the implementation of the remaining parts of the proposal, i.e. Part 2. To that end, I identified the following subtasks:
-
#23738 (closed) T2T (term-to-type) transformation in expressions (at call sites) -
#23739 (closed) T2T (term-to-type) transformation in patterns (at binding sites) -
#24159 (closed) The types-in-terms syntax ( forall
,->
,=>
) -
#23719 (closed) Make forall
a keyword -
#23740 (closed) Term variable capture and implicit quantification
Here are a few examples of code that we aim to allow:
-
A variant of
id
that uses visibleforall
:-- Definition: idv :: forall a -> a -> a idv a x = x :: a -- Usage: n = idv Double 42
This is equivalent to
n = (42 :: Double)
. -
A wrapper around
typeRep
that uses visibleforall
:-- Definition: typeRepVis :: forall a -> Typeable a => TypeRep a typeRepVis a = typeRep @a -- Usage: t = typeRepVis (Maybe String)
-
A wrapper around
sizeOf
that uses visibleforall
instead ofProxy
:-- Definition: sizeOfVis :: forall a -> Storable a => Int sizeOfVis a = sizeOf (Proxy :: Proxy a) -- Usage: n = sizeOfVis Int
-
A wrapper around
symbolVal
that uses visibleforall
instead ofProxy
:-- Definition: symbolValVis :: forall s -> KnownSymbol s => String symbolValVis s = symbolVal (Proxy :: Proxy s) -- Usage str = symbolValVis "Hello, World"
Edited by Vladislav Zavialov