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.