Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Universally vs existentially quantified type variables

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

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]

On the other hand, existential type variables are encoded with a nested forall:

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 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.

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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment