## Modular datatypes and folding for functions

November 5th, 2010 by Laurence E. DayToday 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.

November 6th, 2010 at 10:34 am

It is spelled “à la carte”, not “a la carté”

November 8th, 2010 at 9:53 pm

You’re quite correct! Trust me to hash that one up. Consider it fixed!