# Lambdalog

## Sean Seefried's programming blog

22 Nov 2011

This is an updated version of an earlier post. Owing to a comment by Jed Wesley-Smith I restructured this post somewhat to introduce two techniques for programming with GADTs in Scala. Thanks also go to Tony Morris.

{-# LANGUAGE GADTs #-}module Exp wheredata Exp a where  LitInt  :: Int                        -> Exp Int  LitBool :: Bool                       -> Exp Bool  Add     :: Exp Int -> Exp Int         -> Exp Int  Mul     :: Exp Int -> Exp Int         -> Exp Int  Cond    :: Exp Bool -> Exp a -> Exp a -> Exp a  EqE     :: Eq a => Exp a -> Exp a     -> Exp Booleval :: Exp a -> aeval e = case e of  LitInt i       -> i  LitBool b      -> b  Add e e'       -> eval e + eval e'  Mul e e'       -> eval e * eval e'  Cond b thn els -> if eval b then eval thn else eval els  EqE e e'       -> eval e == eval e'

Here we have defined a data structure that represents the abstract syntax tree (AST) of a very simple arithmetic language. Notice that it ensures terms are well-typed. For instance something like the following just doesn’t type check.

LitInt 1 Add LitBool True -- this expression does not type check

I have also provided a function eval that evaluates terms in this language.

In Scala it is quite possible to define data structures which have the same properties as a GADT declaration in Haskell. You can do this with case classes as follows.

abstract class Exp[A] case class LitInt(i: Int)                                     extends Exp[Int]case class LitBool(b: Boolean)                                extends Exp[Boolean]case class Add(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Mul(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Cond[A](b: Exp[Boolean], thn: Exp[A], els: Exp[A]) extends Exp[A]case class Eq[A](e1: Exp[A], e2: Exp[A])                      extends Exp[Boolean]

But how do we implement eval. You might think that the following code would work. I mean, it looks like the Haskell version, right?

abstract class Exp[A] {  def eval = this match {    case LitInt(i)       => i    case LitBool(b)      => b    case Add(e1, e2)     => e1.eval + e2.eval    case Mul(e1, e2)     => e1.eval * e2.eval    case Cond(b,thn,els) => if ( b.eval ) { thn.eval } else { els.eval }    case Eq(e1,e2)       => e1.eval == e2.eval  }}case class LitInt(i: Int)                                     extends Exp[Int]case class LitBool(b: Boolean)                                extends Exp[Boolean]case class Add(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Mul(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Cond[A](b: Exp[Boolean], thn: Exp[A], els: Exp[A]) extends Exp[A]case class Eq[A](e1: Exp[A], e2: Exp[A])                      extends Exp[Boolean]

Unfortunately for us, this doesn’t work. The Scala compiler is unable to instantiate the type Exp[A] to more specific ones (such as LitInt which extends Exp[Int])

3: constructor cannot be instantiated to expected type;
found   : FailedExp.LitInt
required: FailedExp.Exp[A]
case LitInt(i)       => i
^


There are two solutions to this problem.

# Solution 1: The object-oriented way

You must write eval the object-oriented way. The definition of eval gets spread over each of the sub-classes of Exp[A].

abstract class Exp[A] {  def eval: A}case class LitInt(i: Int)                                     extends Exp[Int] {  def eval = i}case class LitBool(b: Boolean)                                extends Exp[Boolean] {  def eval = b}case class Add(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int] {  def eval = e1.eval + e2.eval}case class Mul(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int] {  def eval = e1.eval * e2.eval}case class Cond[A](b: Exp[Boolean], thn: Exp[A], els: Exp[A]) extends Exp[A] {  def eval = if ( b.eval ) { thn.eval } else { els.eval }}case class Eq[A](e1: Exp[A], e2: Exp[A])                      extends Exp[Boolean] {  def eval = e1.eval == e2.eval}

# Solution 2: The functional Haskell-like way

Personally I don’t like the OO style as much as the Haskell-like style. However, it turns out that you can program in that style by using a companion object.

object Exp {  def evalAny[A](e: Exp[A]): A = e match {    case LitInt(i)         => i    case LitBool(b)        => b    case Add(e1, e2)       => e1.eval + e2.eval    case Mul(e1, e2)       => e1.eval * e2.eval    case Cond(b, thn, els) => if (b.eval) { thn.eval } else { els.eval }    case Eq(e1, e2)        => e1.eval == e2.eval  }}abstract class Exp[A] {  def eval: A = Exp.evalAny(this)}case class LitInt(i: Int)                                     extends Exp[Int]case class LitBool(b: Boolean)                                extends Exp[Boolean]case class Add(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Mul(e1: Exp[Int], e2: Exp[Int])                    extends Exp[Int]case class Cond[A](b: Exp[Boolean], thn: Exp[A], els: Exp[A]) extends Exp[A]case class Eq[A](e1: Exp[A], e2: Exp[A])                      extends Exp[Boolean]

Ah, much better. But why does this work when the previous style doesn’t? The problem is that the constructors are not polymorphic. In Haskell-speak the type is:

LitInt :: Int -> Exp Int

not

LitInt :: Int -> Exp a

The second solution is subtly different. Method evalAny is polymorphic but its type is instantiated to that of the value of whatever it is called on. For instance evalAny when called on LitInt(42) equates type variable A with Int. It can then correctly deduce that it does indeed take a value of Exp[Int] and produce a value of Int.

27 Jun 2011

# Generic dot products

Companion slides

This is the first in a series of posts about program derivation. In particular, I am attempting to derive a matrix multiplication algorithm that runs efficiently on parallel architectures such as GPUs.

As I mentioned in an earlier post, I’ve been contributing to the Accelerate project. The Accelerate EDSL defines various parallel primitives such as map, fold, and scan (and many more).

The scan primitive (also known as all-prefix-sums) is quite famous because it is useful in a wide range of parallel algorithms and, at first glance, one could be forgiven for thinking it is not amenable to parallelisation. However, a well-known work efficient algorithm for scan was popularised by Guy Blelloch which performs $$O(n)$$ work.

The algorithm is undeniably clever. Looking at it, it is not at all obvious how one might have gone about developing it oneself. A recent series of posts by Conal Elliott set out to redress this situation by attempting to derive the algorithm from a high level specification. His success has inspired me to follow a similar process to derive a work efficient matrix multiplication algorithm.

The process I am following is roughly as follows:

• generalise the concept of matrix multiplication to data structures other than lists or arrays.

• develop a generic implementation that relies, as far as possible, on reusable algebraic machinery in type classes such as Functor, Applicative, Foldable and Traversable.

• use this generic implementation as a specification to derive an efficient algorithm. To call it a hunch that the underlying data structure is going to be tree-like is an understatement.

This post is a preamble. It develops a generic dot product implementation that will serve as a specification for the derivation of an efficient algorithm in a later post.

# Background

In order to understand this post I highly recommend that you read Conor McBride and Ross Paterson’s paper: Applicative programming with effects. A basic grasp of linear algebra would also be helpful.

# What is a dot product?

In mathematics the dot product is usually defined on vectors. Given two vectors of length $$n$$, $$(a_1, \dots, a_n)$$ and $$(b_1, \dots, b_n)$$ the dot product is defined as:

$$a_1 b_1 + \dots + a_n b_n$$

or without the use of the pernicious “$$\dots$$”:

$$\sum_{i=1}^{n}{a_i b_i}$$

The implementation for lists is fairly straightforward.

dot :: Num a => [a] -> [a] -> adot xs ys = foldl (+) 0 (zipWith (*) xs ys)

This definition will work just fine on two lists of different length, owing to the definition of zipWith.

zipWith :: (a -> b -> c) -> [a] -> [b] -> [c]zipWith f [] _ = []zipWith f _ [] = []zipWith f (x:xs) (y:ys) = f x y : zipWith f xs ys

This is fine for lists but will become problematic later when we look at other data structures.

There is no reason that this definition shouldn’t be extended to other data structures such as $$n$$-dimensional arrays or even trees. Let’s look at how we might define dot products on trees.

# Dot product on Trees

We define trees as follows (however it does not really matter whether only the leaves contain numbers or whether branch nodes can too):

data Tree a = Leaf a | Branch (Tree a) (Tree a)

For the sake of succinctness, I will represent trees using nested pairs denoted with curly braces. e.g. Branch (Leaf 1) (Leaf 2) becomes {1,2}, Branch (Leaf 1) (Branch (Leaf 2) (Leaf 3)) becomes {1,{2,3}}.

What should be the dot product of {1,{2,3}} and {4,{5,6}}? A reasonable answer would be 1 * 4 + 2 * 5 + 3 * 6 == 32. For each leaf in the first tree find the corresponding leaf in the second tree, multiply them together and then sum all the results together.

This definition relies on the two trees having the same shape. To see why let’s see if we can we define a function in the style of zipWith for trees. Unfortunately, this is problematic.

zipWithT f (Leaf a) (Leaf b)           = Leaf (f a b)zipWithT f (Branch s t) (Branch s' t') = Branch (zipWithT f s s')                                                (zipWithT f t t')zipWithT f (Leaf a) (Branch s' t')     = {- ? -} undefinedzipWithT f (Branch s t) (Leaf b)       = {- ? -} undefined

There’s a problem with the last two cases. While I won’t go so far as to say that there is no definition we could provide, it’s clear that there are a number of choices that could be taken. In each case one needs to take an arbitrary element from the Branch argument and apply function f to it and the Leaf argument.

Even if there is a definition that makes reasonable sense can we say whether it’s possible to provide a zipWith-like definition for an arbitrary data structure?

An alternative is to modify our data structures to contain types that represent the shape of the data structure. We can then define dot such that it must take two arguments of exactly the same shape.

# Data structures with shapes

I’ll illustrate this approach with vectors first, before moving onto trees. Vectors are just lists with their length encode into their type.

## Vectors

First, we add some essentials to the top of our module.

{-# LANGUAGE GADTs, EmptyDataDecls, FlexibleInstances, DeriveFunctor, DeriveFoldable #-}{-# LANGUAGE ScopedTypeVariables, FlexibleContexts, UndecidableInstances #-}

Now we define two new data types, Z and S, representing Peano numbers. Both data types are empty since we will never be using their values.

data Zdata S n

Now vectors.

infixr 5 Consdata Vec n a where  Nil  :: Vec Z a  Cons :: a -> Vec n a -> Vec (S n) a

If you haven’t seen these data types before it’s worth noting that you can define total (vs partial) versions of head and tail. Trying to take the head of an empty vector simply doesn’t type check.

headVec :: Vec (S n) a -> aheadVec (Cons x _) = xtailVec :: Vec (S n) a -> Vec n atailVec (Cons _ xs) = xs

With can now define zipWithV.

zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n czipWithV f Nil Nil = NilzipWithV f (Cons x xs) (Cons y ys) = f x y Cons zipWithV f xs ys

Unfortunately, GHC’s type checker does not detect that a case such as the one below is impossible. (In fact, if your warnings are turned up high enough GHC will warn that two patterns are missing in the definition above.)

-- Although this pattern match is impossible GHC's type checker-- won't complainzipWithV f (Cons x xs) Nil = {- something -} undefined

## Trees

The length of a tree is not quite a meaningful enough representation. Instead we represent its shape as a nested tuples of the unit (()) type.

data Tree sh a where  Leaf   :: a -> Tree () a  Branch :: Tree m a -> Tree n a -> Tree (m,n) a

For example:

{1,{2,3}} :: Tree ((),((),())) Integer

The new definition of zipWithT only differs in its type.

zipWithT :: (a -> b -> c) -> Tree sh a -> Tree sh b -> Tree sh czipWithT f (Leaf a)     (Leaf b)       = Leaf (f a b)zipWithT f (Branch s t) (Branch s' t') = Branch (zipWithT f s s')                                                (zipWithT f t t')

Now finish off the definitions:

foldlT :: (a -> b -> a) -> a -> Tree sh b -> afoldlT f z (Leaf a)     = f z afoldlT f z (Branch s t) = foldlT f (foldlT f z s) tdotT :: Num a => Tree sh a -> Tree sh a -> adotT t1 t2 = foldlT (+) 0 (zipWithT (*) t1 t2

# Generalising to arbitrary data structures

Any seasoned Haskell veteran knows the utility of type classes such as Functor, Applicative, and Foldable. We have now seen that a dot product is essentially a zipWith followed by a fold. (It makes little difference whether its a left or right fold).

Since zipWith is really just liftA2 (found in module Control.Applicative) on the ZipList data structure. This leads us to the following definition:

dot :: (Num a, Foldable f, Applicative f) => f a -> f a -> adot x y = foldl (+) 0 (liftA2 (*) x y)

This function requires instances for Functor, Foldable and Applicative. Given that instances for the first two type classes are both easy to write (and in some cases derivable using Haskell’s deriving syntax), I will only discuss Applicative instances in this post. (The instances for vectors and shape-encoded trees are left as an exercise for the reader.)

One might reasonably wonder, must the two arguments to dot have the same shape as before? It turns out that, yes, they do and for similar reasons. I’ll demonstrate the point by looking at how to define Applicative instances for lists, vectors and trees.

## Lists

The default Applicative instance for lists is unsuitable for a generic dot product. However, the Applicative instance on its wrapper type ZipList is adequate but has an unsatisfying definition for pure (to say the least).

instance Applicative ZipList where  pure x = ZipList (repeat x)  ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

Of course, this is necessary for lists since we can’t guarantee that two lists of the same length will be applied together. How else would you define pure to make it work on an arbitrary length lists xs?

(+) <$> (pure 1) <*> (ZipList xs) The definition of pure is much more satisfying for vectors. ## Vectors Obviously we want a similar definition for pure as for lists (ZipList). But we don’t want to produce an infinite list, just one of the appropriate length. Defining the Applicative instance for vectors leads us to an interesting observation which holds true in general. For any data structure which encodes its own shape: 1. You need one instance of Applicative for each constructor of the data type. 2. The instance heads must mirror the types of the constructors. In the code below there are two instances and each instance head closely mirrors the data constructor’s type. e.g. Cons :: a -> Vec n a -> Vec (S n) a mirrors instance Applicative (Vec n) => Applicative (Vec (S n)). instance Applicative (Vec Z) where pure _ = Nil Nil <*> Nil = Nilinstance Applicative (Vec n) => Applicative (Vec (S n)) where pure a = a Cons pure a (fa Cons fas) <*> (a Cons as) = fa a Cons (fas <*> as) That’s it. Function pure will produce a vector of just the right length. ## Trees Unlike the case for lists, it’s hard to define an Applicative instance for non-shape-encoded trees. Let’s have a look. instance Applicative Tree where pure a = Leaf a (Leaf fa) <*> (Leaf b) = Leaf (fa b) (Branch fa fb) <*> (Branch a b) = Branch (fa <*> a) (fb <*> b) (Leaf fa) <*> (Branch a b) = {- ? -} undefined (Branch fa fb) <*> (Leaf a) = {- ? -} undefined This problem has been noticed before on the Haskell-beginners mailing list. The response is interesting because it mentions the “unpleasant property of returning infinite tree[s]”; the same problem we had with lists! With shape-encoded trees this is not a problem. Function pure produces a tree of the appropriate shape. Also, note how the head of the second instance mirrors the definition of the Branch constructor (:: Tree m a -> Tree n a -> Tree (m,n) a) instance Applicative (Tree ()) where pure a = Leaf a Leaf fa <*> Leaf a = Leaf (fa a)instance (Applicative (Tree m), Applicative (Tree n)) => Applicative (Tree (m,n)) where pure a = Branch (pure a) (pure a) (Branch fs ft) <*> (Branch s t) = Branch (fs <*> s) (ft <*> t) # Arbitrary binary associative operators. Phew, that’s it. We now have an implementation for dot that will work on an arbitrary data structure as long as one can define Functor, Foldable and Applicative instances. We have also learned that it is a good idea to encode the data structure’s shape in its type so that Applicative instances can be defined. (This will be important later on when we want to take the transpose of generic matrices, but I’m getting ahead of myself.) But what if you want to use binary associative operators other than addition and multiplication for the dot product? This is easy using Haskell’s Monoid type class, and it plays nicely with the Foldable type class. In fact, it allows us to omit any mention of identity elements using the method fold:: (Foldable t, Monoid m) => t m -> m. We define an even more generic dot product as follows: dotGen :: (Foldable f, Applicative f, Monoid p, Monoid s) => (a -> p, p -> a) -> (a -> s, s-> a) -> f a -> f a -> adotGen (pinject, pproject) (sinject, sproject) x y = sproject . fold . fmap (sinject . pproject)$ liftA2 mappend px py  where    px = fmap pinject x    py = fmap pinject y

This function takes two pairs of functions for injecting into and projecting from monoids. We can then define our original dot function using the existing Sum and Product wrapper types.

dot :: (Num a, Foldable f, Applicative f) => f a -> f a -> adot = dotGen (Product, getProduct) (Sum, getSum)

# In the next episode…

In my next post we will consider generic matrix multiplication. This operation is defined over arbitrary collections of collections of numbers and, naturally, makes use of our generic dot product. Until then, adios.

# Slides

On 17 Nov 2011 I gave a talk at fp-syd about this work. You can find the slides here.

16 May 2011

# Reifying Type Classes with GADTs

This year I’ve been contributing to Accelerate, an embedded language for regular, multi-dimensional array computations targetting high-performance back-ends such as NVIDIA GPUs. Even a cursory glance of the code base shows that it uses a number of advanced Haskell extensions including Generalized Algebraic Data Types (GADTs) and type families.

Earlier this year I learned a technique which seems to be part of the Haskell folklore but not necessarily well known: reifying types belonging to a type class into a GADT value. A typical use-case for this technique is using a type class defined in a library. Either you don’t have access to the source code (or for reasons of modularity/API stability you don’t want to touch it) but, nevertheless, you want to add a method to the type class. For argument’s sake let’s call this type class C.

The standard solution would be to declare a new type class, let’s call it D, with a super-class constraint on class C. (e.g. class C a => D a). You would then have to write one instance of class D for each existing instance of class C. Not only could this be a lot of work, you could run into the same problem of needing to extend class D further down the track (perhaps necessitating the declaration of class E).

What if there were a way to allow class C to be arbitrarily extensible? This being a blog post on the topic, it should come as no surprise that there is, with one caveat: the class must be closed. That is, the instances that have been written are complete and will not need to be changed in the future.

I’ll demonstrate how to reify types into values of a GADT using an example. Say we have a class, Counter, with a single method inc to increment a value.

{-# LANGUAGE GADTs #-}class Counter a where  inc :: a -> a

Here are all the instances we will ever write for this class.

data CounterR a where  CounterRint  :: CounterR Int  CounterRchar :: CounterR Char  CounterRlist :: CounterR a -> CounterR [a]  CounterRpair :: CounterR a -> CounterR b -> CounterR (a,b)class Counter a where  inc :: a -> ainstance Counter Int where  inc a = a + 1instance Counter Char where  inc a = chr (ord a + 1)instance Counter a => Counter [a] where  inc as = map inc asinstance (Counter a, Counter b) => Counter (a,b) where  inc (a,b) = (inc a, inc b)

Although the instances are fixed, we wish to allow others to effectively add new methods to the class in the future. We can do this by declaring a GADT that reifies the instance types. By convention we name this data structure by appending the character R to the class name.

data CounterR a where  CounterRint  :: CounterR Int  CounterRchar :: CounterR Char  CounterRlist :: CounterR a -> CounterR [a]  CounterRpair :: CounterR a -> CounterR b -> CounterR (a,b)

Please note the following properties of this declaration:

• There is one constructor for each instance of class Counter.

• Every constraint on the Counter class in an instance declaration becomes a parameter of the corresponding GADT constructor. e.g. instance (Counter a, Counter b) => Counter (a,b) becomes CounterRpair :: CounterR a -> CounterR b -> CounterR (a,b).

We now need to add a new method signature to class Counter and provide an implementation for it in each of the instances. By convention this method is called counterR; that is, the name of the class with the first letter lower-cased and suffixed with character ‘R’.

Our module so far looks like this:

{-# LANGUAGE GADTs, FlexibleInstances, UndecidableInstances #-}module Counter whereimport Data.Chardata CounterR a where  CounterRint  :: CounterR Int  CounterRchar :: CounterR Char  CounterRlist :: CounterR a -> CounterR [a]  CounterRpair :: CounterR a -> CounterR b -> CounterR (a,b)class Counter a where  inc :: a -> a  counterR :: CounterR ainstance Counter Int where  inc a = a + 1  counterR = CounterRintinstance Counter Char where  inc a = chr (ord a + 1)  counterR = CounterRcharinstance Counter a => Counter [a] where  inc as = map inc as  counterR = CounterRlist counterRinstance (Counter a, Counter b) => Counter (a,b) where  inc (a,b) = (inc a, inc b)  counterR = CounterRpair counterR counterR

Note that definition of counterR for each instance follows a very simple pattern. It is simply the application of the appropriate constructor to the appropriate number of calls to counterR.

It’s important to be clear that values of CounterR a don’t represent values of type a, they represent the type a itself.

For instance a value of type

CounterR (([Int], Int), (Int, Char))

reifies to the value

CounterRpair  (CounterRpair (CounterRlist CounterRint) CounterRint))  (CounterRpair CounterRint CounterRchar)

We can now write new methods on any type that is a member of class Counter. I’ll show you with an example. Say we now want to write a function that decrements instead of incrementing. We can write this as follows, but please note that the function takes the representation of the type and the value as an argument.

dec :: CounterR a -> a -> adec CounterRint a                    = a - 1dec CounterRchar a                   = chr (ord a - 1)dec (CounterRlist incRa) as          = map (dec incRa) asdec (CounterRpair incRa incRb) (a,b) = (dec incRa a, dec incRb b)

There are only a few things to note:

• If dec were a method of class Counter then you would need to define it in each instance. Here you provide each implementation as a case of the dec function.
• Since dec requires a value of type CounterR each recursive call to dec requires that you pass an appropriate value of type CounterR. Fortunately, the appropriate value is precisely one of those pattern matched on the left hand side.

As I noted at the beginning. This technique is not new, just relatively unknown. A paper by Oliveira and Sulzmann suggests unifying the two concepts. Also, GADTs have been used as an implementation technique in JHC instead of the normal dictionary passing implementation.