Haskell existential quantification in detail

Question

I have a general idea of what existential quantification on types is and where it can be used. However from my experiences so far, there are a lot of caveats that need to be understood in order to use the concept effectively.

Question: Are there any good resources explaining how existential quantification is implemented in GHC? I.e.

• How does unification on existential types work - what is unifiable and what is not?
• In what order subsequent operations on types are performed?

My aim is to better understand error messages that GHC throws at me. Messages usually say something along the lines "this type using forall and this other type don't match", however they don't explain why it is so.

Answer 1

The nitty-gritty details are covered in papers from Simon Peyton-Jones, though it takes a good deal of technical expertise to understand them. If you want to read a paper on how Haskell type inference works, you should read about generalized algebraic data types (GADTs), which combine existential types with several other features. I suggest "Complete and Decidable Type Inference for GADTs", on the list of papers at http://research.microsoft.com/en-us/people/simonpj/.

Existential quantification actually works a lot like universal quantification. Here is an example to highlight the parallels between the two. The function useExis is useless, but it's still valid code.

data Univ a = Univ a
data Exis = forall a. Exis a

toUniv :: a -> Univ a
toUniv = Univ

toExis :: a -> Exis
toExis = Exis

useUniv :: (a -> b) -> Univ a -> b
useUniv f (Univ x) = f x

useExis :: (forall a. a -> b) -> Exis -> b
useExis f (Exis x) = f x

First, note that toUniv and toExis are nearly the same. They both have a free type parameter a because both data constructors are polymorphic. But while a appears in the return type of toUniv, it doesn't appear in the return type of toExis. When it comes to the kind of type errors you might get from using a data constructor, there's not a big difference between existential and universal types.

Second, note the rank-2 type forall a. a -> b in useExis. This is the big difference in type inference. The existential type taken from the pattern match (Exis x) acts like an extra, hidden type variable passed to the body of the function, and it must not be unified with other types. To make this clearer, here are some wrong declarations of the last two functions where we try to unify types that shouldn't be unified. In both cases, we force the type of x to be unified with an unrelated type variable. In useUniv, the type variable is part of the function type. In useExis, it's the existential type from the data structure.

useUniv' :: forall a b c. (c -> b) -> Univ a -> b
useUniv' f (Univ x) = f x -- Error, can't unify 'a' with 'c'
                          -- Variable 'a' is there in the function type

useExis' :: forall b c. (c -> b) -> Exis -> b
useExis' f (Exis x) = f x -- Error, can't unify 'a' with 'c'.
                          -- Variable 'a' comes from the pattern "Exis x",
                          -- via the existential in "data Exis = forall a. Exis a".