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 ON THE LEFT of a type signature:
head :: forall a. [a] -> Maybe a
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
-- call `head` result = head @Int [1,2]
On the other hand, existential type variables are encoded with a nested
printSomeStuff :: (forall a. Show a => a -> String) -> IO () printSomeStuff printFunction = do putStrLn (printFunction @Int 123) putStrLn (printFunction @Char 'c')
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 with a GADT:
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.
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
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