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:

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:

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:

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

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:

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:

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

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

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

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:

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).

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.

Haskeller Haskelling.

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store