Nottingham FP Lab Blog

Modular datatypes and folding for functions

by Laurence E. Day on November 5, 2010.
Tagged as: Lunches.

Today I presented part of Wouter Swierstra’s “Data types à la carte” (thanks for the correction, French guy!) paper (JFP 2008). To this end, I showed a solution to the expression problem by way of modularising datatypes with coproducts of type constructors and constructing initial algebras for generic functor folds as a supported operation of a type-class, as well as a method for defining ‘smart constructors’. By way of explanation, I defined a function isomorphic to the traditional evaluate function on integers and addition. Discussion then (predictably!) turned towards implementing these ideas in Agda – interest seemed quite high.

data Fix f = In (f (Fix f)) data (f :+: g) e = Inl (f e) | Inr (g e)

fold :: Functor f => (f a -> a) -> Fix f -> a
fold f (In t) = f (fmap (fold f) t)

data Val e = Val Int
data Add e = Add e e
type Expr = Fix (Val :+: Add)

For the class constraint on the fold operation to be satisfied, we need the both the type constructor coproduct and all components to be functors themselves.

instance (Functor f, Functor g) => Functor (f :+: g) where fmap f (Inl x) = Inl (fmap f x) fmap g (Inr y) = Inr (fmap g y)

instance Functor Val where
fmap f (Val n) = Val n

instance Functor Add where
fmap f (Add x y) = Add (f x) (f y)

We declare our evaluator algebra as a supported operation of a typeclass defined for an arbitrary functor.

class (Functor f) => Eval f where
  evalAlg :: f Int -> Int

instance (Eval f, Eval g) => Eval (f :+: g) where
  evalAlg (Inl x)  = evalAlg x
  evalAlg (Inr y)  = evalAlg y

instance Eval Val where
  evalAlg (Val n) = n

instance Eval Add where
  evalAlg (Add x y) = x + y

eval               :: (Eval f) => Fix f -> Int
eval               = fold evalAlg

In order to define the smart constructors for manipulating data in this format, we need to define a subtyping relation with (unfortunately) a pair of overlapping instances.

class (Functor sub, Functor sup) => sub :<: sup where
  inj :: sub a -> sup a

instance (Functor f) => (:<:) f f where
  inj = id

instance (Functor f,
          Functor g) => (:<:) f (f :+: g) where
  inj = Inl

instance (Functor f,
          Functor g,
          Functor h,
          (:<:) f g) => (:<:) f (h :+: g) where
  inj = Inr . inj

We're now in a position where we can easily define both a carrier function into a supertype (inject) and smart constructors for our language.

inject      :: (g :<: f) => g (Fix f) -> Fix f
inject      = In . inj

val         :: ((:<:) Val f) => Int -> Fix f
val n       = inject (Val n)

add         :: ((:<:) Add f) => Fix f -> Fix f -> Fix f
n `add` m   = inject (Add n m)

Now we can very easily define instances of the Expr datatype and evaluate them just as we would expect to if our datatype was defined in the standard way:

example :: Expr example = val 18 `add` val 24

> eval example
> 42

I wish to use the work presented here as part of a framework upon which to construct a compiler fully modular in its source/target languages and the computations it supports.