What is this GHC feature called? `forall` in type definitions

user_55246 0
Viewed 117

I learned that you can redefine ContT from transformers such that the r type parameter is made implicit (and may be specified explicitly using TypeApplications), viz.:

-- | Same as `ContT` but with the `r` made implicit
type ContT ::
  forall (r :: Type).
  (Type -> Type) ->
  Type ->
  Type
data ContT m a where
  ContT ::
    forall r m a.
    {runContT :: (a -> m r) -> m r} ->
    ContT @r m a

type ContVoid :: (Type -> Type) -> Type -> Type
type ContVoid = ContT @()

I hadn't realized this was possible in GHC. What is the larger feature called to refer to this way of defining a family of types with implicit type parameters, that is specified using forall in type definition (referring, in the example above, to the outer forall - rather than the inner forall which simply unifies the r)?

forall ghc haskell
1 Answers

Nobody uses this (invisible dependent quantification) for this purpose (where the dependency is not used) but it is the same as giving a Type -> .. parameter, implicitly.

type EITHER :: forall (a :: Type) (b :: Type). Type
data EITHER where
 LEFT  :: a -> EITHER @a @b
 RIGHT :: b -> EITHER @a @b

eITHER :: (a -> res) -> (b -> res) -> (EITHER @a @b -> res)
eITHER left right = \case
 LEFT  a -> left  a
 RIGHT b -> right b

You can also use "visible dependent quantification" where forall-> is the visible counterpart to forall., so forall (a :: Type) -> .. is properly like Type -> .. where a does not appear in ..:

type EITHER :: forall (a :: Type) -> forall (b :: Type) -> Type
data EITHER a b where
 LEFT  :: a -> EITHER a b
 RIGHT :: b -> EITHER a b

eITHER :: (a -> res) -> (b -> res) -> (EITHER a b -> res)
eITHER left right = \case
 LEFT  a -> left  a
 RIGHT b -> right b
user_1658060
Related