In this section, we will describe a series of patterns related to data abstraction. We start with existentially quantified types then progress to phantom types and end with GADTs. We'll see that these patterns fall within a spectrum of generality and power.
Let's explore existential quantification from the perspective of its opposite, universal quantification.
All parametrically polymorphic functions, from Rank 1
to higher rank functions, are universally quantified. Similarly, parametrically polymorphic datatypes are universally quantified. If the Haskell syntax for universally quantified functions and datatypes were consistent, then we would have had to use the forall
keyword in datatype signatures to indicate polymorphism, for example:
data Maybe' a = Nothing' | Just' a
-- conceptually (but not practically!) the same as
data Maybe' a = forall a. Nothing' | Just' a
As another example, consider the universally quantified type...