Haskell Language Common GHC Language Extensions ExistentialQuantification
Example
This is a type system extension that allows types that are existentially quantified, or, in other words, have type variables that only get instantiated at runtime†.
A value of existential type is similar to an abstract-base-class reference in OO languages: you don't know the exact type in contains, but you can constrain the class of types.
data S = forall a. Show a => S a
or equivalently, with GADT syntax:
{-# LANGUAGE GADTs #-}
data S where
S :: Show a => a -> S
Existential types open the door to things like almost-heterogenous containers: as said above, there can actually be various types in an S value, but all of them can be shown, hence you can also do
instance Show S where
show (S a) = show a -- we rely on (Show a) from the above
Now we can create a collection of such objects:
ss = [S 5, S "test", S 3.0]
Which also allows us to use the polymorphic behaviour:
mapM_ print ss
Existentials can be very powerful, but note that they are actually not necessary very often in Haskell. In the example above, all you can actually do with the Show instance is show (duh!) the values, i.e. create a string representation. The entire S type therefore contains exactly as much information as the string you get when showing it. Therefore, it is usually better to simply store that string right away, especially since Haskell is lazy and therefore the string will at first only be an unevaluated thunk anyway.
On the other hand, existentials cause some unique problems. For instance, the way the type information is “hidden” in an existential. If you pattern-match on an S value, you will have the contained type in scope (more precisely, its Show instance), but this information can never escape its scope, which therefore becomes a bit of a “secret society”: the compiler doesn't let anything escape the scope except values whose type is already known from the outside. This can lead to strange errors like Couldn't match type ‘a0’ with ‘()’ ‘a0’ is untouchable.
†Contrast this with ordinary parametric polymorphism, which is generally resolved at compile time (allowing full type erasure).
Existential types are different from Rank-N types – these extensions are, roughly speaking, dual to each other: to actually use values of an existential type, you need a (possibly constrained-) polymorphic function, like show in the example. A polymorphic function is universally quantified, i.e. it works for any type in a given class, whereas existential quantification means it works for some particular type which is a priori unknown. If you have a polymorphic function, that's sufficient, however to pass polymorphic functions as such as arguments, you need {-# LANGUAGE Rank2Types #-}:
genShowSs :: (∀ x . Show x => x -> String) -> [S] -> [String]
genShowSs f = map (\(S a) -> f a)
