Faking it with higher rank (Existential Quantification pt. 2)

In my previous post I provided a short background on Existential Quantification.  In this post, I'll provide an alternative for some uses and suggest why it may be preferred.

Suppose we want to create a data store that uses lists for small amounts of data, but otherwise uses vectors.  We can easily use E.Q.

import Data.Vector (Vector)
import qualified Data.Vector as V
class Buffer c where
  type El c :: *
  init :: Int -> El c -> c
  (!)  :: c -> Int -> El c
  push :: c -> El c -> c
 
instance Buffer [a] where
  type El [a] = a
  init = replicate
  (!)  = (!!)
  push lst el = el : init lst
 
instance Buffer (Vector a) where
  type El (Vector a) = a
  init = V.replicate
  (!)  = (V.!) 
  push vec el = V.cons el $ V.unsafeInit vec
 
data EBuffer a = forall c. (Buffer c, El c ~ a) => EBuffer c
 
initBuffer :: Int -> EBuffer Double
initBuffer sz
  | sz < 10   = EBuffer (init sz 0 :: [Double])
  | otherwise = EBuffer (init sz 0 :: Vector Double)
 

and now we have our existentially-quantified buffer.

Unfortunately this code doesn't offer anywhere near the hoped-for performance (at least not for the problem that led to this post).  The problem is that now that the actual type of buffer is hidden in the EBuffer data, the compiler is no longer able to inline function calls to (!) or push.  Instead it needs to go through the dictionary methods, adding a lot of extra overhead.  Even worse, a lot of further optimization opportunities are lost.

It turns out that there is another approach that doesn't suffer from this problem.  The approach is based on higher-rank types.  Normal Haskell code uses rank-1 type variables, which means that any variables in a type signature are instantiated by the calling code.  However, with the RankNTypes extension, it's possible to write code of any rank desired.  Consider the function

hr1 :: (forall a. a -> a) -> (Char, Int)
hr1 myId = (myId 'a', myId 0)

The first parameter to hr1 is a rank-2 function.  It needs to be a function that can take an input of any type, and return a value with the same type.  The only total function that can do this is id, and calling hr1 id returns exactly what we would expect.

(What happens if you change the type signature to hr1 :: (a -> a) -> (Char, Int) ? )

Armed with higher-rank types, we can replace the existentially-quantified type in two steps:

1.  Refactor whichever code uses the data so that it's in the form someFunc :: Buffer buf => buf -> AResult.  This part usually isn't too difficult.

2.  Create another function like following:

runWithBuffer
  :: Int
  -> (forall buf. (Buffer buf, El buf ~ Double) => buf -> b)
  -> b
runWithBuffer sz fn
  | sz < 10   = let buf = init sz 0 :: [Double]
                in fn buf
  | otherwise = let buf = init sz 0 :: Vector Double
                in fn buf

With our new runWithBuffer function, we've successfully decoupled the buffer selection algorithm from the usage site without using existential quantification.  Plus, in many cases GHC generates better code with more opportunities for further optimization.

A slightly more extensive example is available in my dsp-extras codebase.  The class and various buffer types are in the Data.RingBuffer modules.  The buffers are used in Language.AuSL.CompileArr, with the function optimizeBufType performing the duties of runWithBuffer.

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.

J. Roger Hindley is coming to Maynooth

I have recently learned that J. Roger Hindley (of Hindley-Milner) will be giving a talk next month on the history of Curry-Howard in the Mathematics Dept. at NUI Maynooth.  I will definitely be there!