Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Haskell existential quantification in detail

Tags:

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.

like image 811
julx Avatar asked Feb 13 '12 11:02

julx


People also ask

What does forall mean in Haskell?

forall is something called "type quantifier", and it gives extra meaning to polymorphic type signatures (e.g. :: a , :: a -> b , :: a -> Int , ...). While normaly forall plays a role of the "universal quantifier", it can also play a role of the "existential quantifier" (depends on the situation).

What is an existential type?

Existential types, or 'existentials' for short, are a way of 'squashing' a group of types into one, single type. Existentials are part of GHC's type system extensions.

What is existential type in Swift?

Existentials in Swift allow defining a dynamic value conforming to a specific protocol. Using primary associated types, we can constrain existentials to certain boundaries. The Swift team introduced the any keyword to let developers explicitly opt-in to a performance impact that might otherwise not be visible.


1 Answers

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".
like image 195
Heatsink Avatar answered Sep 27 '22 17:09

Heatsink