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
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.