A type variable can be either universally ("for all x, then ...") or existentially quantified ("there exists some x, ...").
(If you're a maths persons, this corresponds to ∀x. x
and ∃x. x
, respectively)
In haskell, universally quantified type vars are represented with a forall
:
head :: forall a. [a] -> Maybe a
Here, a
is universally quantified. This means that the CALLER of head
can choose what they want a
to be.
So, as the caller, I can say I want a=Int
:
-- call `head`
result = head @Int [1,2]
printSomeStuff :: (forall a. Show a => a -> String) -> IO ()
printSomeStuff printFunction = do
putStrLn (printFunction @Int 123)
putStrLn (printFunction @Char 'c')
Here, a
is existentially quantified. This means the the CALLER can't choose a
anymore. It's the function itself that will choose what it wants a
to be.
You can see in the implementation that the function decided it wanted a=Int
and then a=Char
later on.
But the caller has no way of knowing what a
will be:
result = printSomeStuff show
Basically, it inverts the responsabilities between the caller and the callee.
Another common way of encoding existential type variables is:
{-# LANGUAGE ExistentialQuantification #-}
data Showable = forall a. Show a => MkShowable a
-- or
{-# LANGUAGE GADTSyntax #-}
data Showable where
MkShowable :: forall a. Show a => a -> Showable
The type variable a
appears in the MkShowable
constructor signature, but NOT in the type. The type is just Showable
, it has no type variables.
Essentially, the MkShowable
constructor stores a type variable a
inside of it and "hides" it.
listOfShowables :: [Showable]
listOfShowables = [MkShowable @Int 1, MkShowable @Char 'c']
So, when a Showable
is passed to you, you have no way of knowing what type variable is stored inside of it:
f :: Showable -> IO ()
f showable = do
-- is this showable an int? a char? something else?
pure ()
All we know is that there exists some variable inside the MkShowable
constructor, and that it has a Show
constraint.
So all you can do is literally print that value.
There's absolutely nothing else you can do with it.
f :: Showable -> IO ()
f showable = do
case showable of
MkShowable v ->
-- We don't know what the type of `v` is at compile time, it could be anything.
-- All we know is that it has a Show constraint.
putStrLn $ show v
This is a little imprecise. The definition in question only uses
ExistentialQuantification
andGADTSyntax
, not GADTs proper. You could rewrite it withoutGADTSyntax
, too:(that said, GADTs are basically a syntax sugar for type equivalence constraints, so you could have "proper" GADTs without the GADT syntax, too)