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.

comments powered by Disqus