Universally vs existentially quantified type variables

universal_existential.md

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

Another common way of encoding existential type variables is with a GADT

This is a little imprecise. The definition in question only uses ExistentialQuantification and GADTSyntax, not GADTs proper. You could rewrite it without GADTSyntax, too:

data Showable = forall a. Show a => MkShowable a

(that said, GADTs are basically a syntax sugar for type equivalence constraints, so you could have "proper" GADTs without the GADT syntax, too)

@lierdakil yeah, this was kind of a braindump I did in 10mins in a very informal way 😅 I've fixed this now