Saturday, March 24, 2012

Existential Quantification pt. 1

If you have experience with OOP, you're already an expert on existential quantification.  In brief, existential quantification is the reason why you can write code like this pseudocode:

class MyList: 
  private List myList;
  init(Int sz):
    if sz < 10: 
      self.myList = new LinkedList();
    else:
      self.myList = new ArrayList();

In this example the private member variable myList is existentially quantified.  For any instance of MyList, after init is called the compiler knows that a data structure exists and that it implements the List interface, but it doesn't know the exact type of myList.  Any time you declare a variable of an interface type, the data structure referenced by the variable is existentially quantified.

One of the most common uses of existentially quantified data is in implementing the Strategy design pattern, which allows for an algorithm to be selected at runtime.  The MyList class above hints at this usage; for very small lists it uses a LinkedList but otherwise uses an ArrayList.  The idea of selecting an optimal algorithm at runtime based upon some known quantity is very common in high-performance code (e.g. fftw, Atlas, introsort, many others), and existential quantification is a very common way to implement it.

It's very common for programmers with an OOP background to assume that existential quantification and interfaces always go together, which leads to surprise that the following Haskell code doesn't compile:

getNum :: Num a => Char -> a
getNum 'd' = 0 :: Double
getNum _  = 0 :: Int

In OOP languages, this works.  Both Double and Int are instances of Num, and the only promise the type of getNum makes about its output is that it has a Num instance.  However, type variables aren't existentially quantified in Haskell.  This means that, instead of returning whichever Num instance it likes, getNum must be able to provide any Num that the caller demands.

However, thanks to the ExistentialQuantification language extension, e.q. is supported in Haskell (GADTs also provide this feature and more).  It can only be used within new data types however, not bare functions.  So we need to make a wrapper to hold existentially quantified data:
{-# LANGUAGE ExistentialQuantification #-}
data ENum = forall a. Num a => ENum a

getNum :: Char -> ENum
getNum 'd' = ENum (0::Double)
getNum _   = ENum (0::Int)

Now we have our existentially-quantified data, and all is right with the world.  For now.

No comments:

Post a Comment