Existential Quantification Patterns and Antipatterns

ExistentialQuantification let’s one hide a type variable. One would do this to manipulate different types of values in a uniform way.

The Existential Type Class Antipattern

It is almost a rite of passage in Haskell to recreate the Existential Type Class Antipattern. Here’s how this happens.

You want to make a list of things that you can show like:

map show [1, 'h', True] -- This won't compile

Except Haskell can’t directly create a list of different types. However, you can make a list of showable things. ExistentialQuantification helps you do that:

data Showable = forall a. Show a => Showable a
instance Show Showable where
  show (Showable x) = show x

Showable is a type that hides the type of a using existential quantification that must have a Show instance. We can now create a list of Showable things:

map show [Showable 1, Showable 'h', Showable True] -- compiles!

So all seems good, except it was a very indirect way to write:

[show 1, show 'h', show True]

Worse, types with existentials are not standard types, so working with them is more difficult than Haskell 2010 types (notice above I could not derive the Show instance).

The existential type class antipattern delays the use of type class methods with an additional wrapper type, but we can just make the function calls ahead of time. If we truly need to delay the execution of a method, we can without much work: Haskell is lazy.

Pattern 1: Intermediate Value

Once you realize that creating a uniform type for type class method application is not a good use of type classes, it begs the question of what a good use is.

The Intermediate Value pattern is a way to hide an unnecessary type that is used internally by a function(s).

A good example is the Fold type from the foldl package:

data Fold a b
  -- | @Fold @ @ step @ @ initial @ @ extract@
  = forall x. Fold (x -> a -> x) x (x -> b)

The Fold type holds an initial value, x (the second argument to the constructor). The first time the “step” (first argument) is called, it is passed the initial x and the result of “step” is feedback to itself over and over again. Finally, at the end of the computation the result of the "step” (an x) is converted to a b by the final “extract” argument.

After creating a Fold, there is no way to tell what the type of x is. This is fine though. All that matters is that x is the same type as needed by the “step” and “extract” functions.

There is no need to expose the type of x. If the Fold was Fold x a b instead of Fold a b, it would make the library unnecessarily complicated to use (and in some cases impossible to write see), with no real benefit.

Another example of this pattern is the free applicative (hat tip to David Reaver).

Pattern 2: Hidden Types Which Can Unhidden

The basic rule is that when one hides a type with an existential, it cannot be retrieved. However, this is not the whole story.

GHC has a feature called type equality, which is turned on by several extensions, one being GADTs.

With type equality I can write the constructor:

data Hideable a = a ~ Int  => IntHideable a 
                | a ~ Char => CharHideable

Then I can hide the a with a new type and an existential:

data AnyHideable = forall a. AnyHideable (Hideable a)

If I pattern match on a AnyHideable I won’t know what type of Hideable I have.

incHideable :: Hideable Int -> Int
incHideable (IntHideable x) = x + 1
foo :: AnyHideable -> IO ()
foo (AnyHideable x) = case x of -- x is of type Hideable a
...

However, when I pattern match on the constructor IntHideable it will bring the constraint a ~ Int constraint into scope.

incHideable :: Hideable Int -> Int
incHideable (IntHideable x) = x + 1
foo :: AnyHideable -> IO ()
foo (AnyHideable x) = case x of
  IntHideable {} -> print $ incHideable x -- x is a (Hideable Int)
  ... 

At this point, the compiler will know that the Hideable a is actually a Hideable Int and I can use incHideable on it.

Alright, so this is a contrived example. The point is that we can go from a uniform type AnyHideable and regain the type information of the Hideable's a. The existentially quantified AnyHideable can be nice because we treat it uniformly, but if we want to operate on the specific Hideable, we can do that through pattern matching.

Most Haskeller’s have not seen type equality used this way, but that is because GHC has nice syntax for types like this, mainly GADT syntax. The same type written with GADT syntax looks like:

data Hideable a where
  IntHideable  :: Int  -> Hideable Int
  CharHideable :: Char -> Hideable Char

Under the hood, the same type equality magic is happening.

Update May 29: David Feuer pointed on reddit that there a few other examples I discuss below.

Pattern 3: Type Aligned Data Structures

Type aligned data structures allow one to create lists, sequences, trees and other data structures, where new data and old data’s types match up.

Here I create a type aligned list for well typed paths between TCP states. I create a kind and separate types for the states (State), and each transition or arrow in a state diagram is constructor in GADT (the Path type).

data State = Closed | Listen | SynSent | SynReceived | Established
           | CloseWait | LastAck | FinWait1 | FinWait2 | Closing
           | TimeWait
data Path :: State -> State -> * where
  ServerStart          :: Path Closed      Closed
  PassiveOpen          :: Path Closed      Listen
  ServerClose          :: Path Listen      Closed
  ServerSynRecieved    :: Path Listen      SynReceived
  ClientSynRecieved    :: Path SynReceived SynReceived
  SynResponded         :: Path SynReceived Established
  ToFinWait1           :: Path Established FinWait1
  ActiveOpen           :: Path Closed      SynSent
  PassiveToActive      :: Path Listen      SynSent
  ClientClose          :: Path SynSent     Closed
  FinishHandshake      :: Path SynSent     Established
  PassiveClose         :: Path Established CloseWait
  ToLastAck            :: Path CloseWait   LastAck
  EarlyClose           :: Path SynReceived FinWait1
  ActiveClose          :: Path Established FinWait1
  SimulatanousClose    :: Path FinWait1    Closing
  SimulatanousCloseAck :: Path Closing     TimeWait
  FastClose            :: Path FinWait1    TimeWait
  CloseAcknowledge     :: Path FinWait1    FinWait2
  FinishClose          :: Path FinWait2    TimeWait
  Waited               :: Path TimeWait    Closed
  (:::)                :: Path a b -> Path b c -> Path a c
  
connectAndClose :: Path Closed Closed
connectAndClose = ServerStart ::: ActiveOpen ::: ClientClose

Existential quantification is used implicitly in the ::: constructor to hide the intermediate types (the b). connectAndClose is an example of valid path that goes through Closed, SynSent, and back to Closed states. The intermediates state SynSent must match up, but is not visible in the connectAndClose type.

Type aligned data structures can be used to create more precisely type programs and can result in algorithmic improvements (see Reflection Without Remorse).

Relation to RankNTypes

Existential quantification uses forall syntax in an almost indistinguishable way fromRankNTypes. This leads many Haskellers to conclude that they are similar extensions. Although existential quantification uses the same syntax, it is used for different goals (even if, yes, higher rank polymorphism can encode existential quantification).

Conclusion

ExistentialQuantification is GHC’s way of hiding type information. In the some situations, this information can be regained, or one can hide the information along with functions to operate on the hidden type. If one stays away from the Existential Type Class Antipattern, there is a chance that ExistentialQuantification won’t get used that often. This is normal.