Wed 26 Mar 2008

## Higher-Order Abstract Syntax à la Carte

Posted by Edward Kmett under Category Theory , Haskell[2] Comments

You may recall the definition for an exponential functor from my previous entry, which can also be viewed, I suppose, as functors in the

category of right-invertible functions in Haskell.

class ExpFunctor f where xmap :: (a -> b) -> (b -> a) -> f a -> f b

Clarifying the above, an instance of ExpFunctor should satisfy the slightly generalized version of the Functor laws from Control.Monad:

xmap id id = id xmap f g . xmap f' g' = xmap (f . f') (g' . g)

Since we like to apply xmap to a pair of functions such that f . g = id, as in the Fegaras/Sheard case, we get:

xmap f g . xmap g f = xmap (f . g) (f . g) -- by second xmap law = xmap id id -- by f . g = id = id -- by first xmap law

In any event, what I thought what I'd do today is note that Wouter Swierstra's Data Types a la Carte approach works over exponential functors.

Swierstra's main definition looks something like:

data (f :+: g) e = Inl (f e) | Inr (g e) instance (Functor f, Functor g) => Functor (f :+: g) where fmap f (Inl e) = Inl (fmap f e) fmap f (Inr e) = Inr (fmap f e)

This permits the obvious analogue:

instance (ExpFunctor f, ExpFunctor g) => ExpFunctor (f :+: g) where xmap f g (Inl e) = Inl (xmap f g e) xmap f g (Inr e) = Inr (xmap f g e)

With this we can quickly encode the untyped lambda calculus:

newtype Lam a = Lam (a -> a) instance ExpFunctor Lam where xmap f g (Lam k) = Lam (f . k . g) data App a = App a a instance Functor App where fmap f (App a b) = App (f a) (f b) instance ExpFunctor App where xmap = const . fmap

(Even better we could define a generic Bind and Binary functors, and newtype to get Lam and App)

and we can encode the recursion using any of the ways we previously established to tie the knot (Nu f, ForAll (Rec f), ForAll (Elim f)).

The rest of the a la carte stuff remains unchanged.

We then get a definition of catamorphism 'for free', due to the definitions from the other day.

From there we can define a fairly generic pretty printing framework.

class ShowAlgebra f where showAlgebra :: f ([String] -> String) -> [String] -> String instance (ShowAlgebra f, ShowAlgebra g) => ShowAlgebra (f :+: g) where showAlgebra (Inl e) = showAlgebra e showAlgebra (Inr e) = showAlgebra e instance (Cata f (ForAll t), ShowAlgebra f) => Show (ForAll t) where show x = cata showAlgebra (runForAll x) vars

And then we can derive particular instances for the untyped lambda calculus we slapped together above:

instance ShowAlgebra Lam where showAlgebra (Lam k) (v:vars) = "(\\\\" ++ v ++ ". " ++ k (const v) vars ++ ")" instance ShowAlgebra App where showAlgebra (App a b) vars = "(" ++ a vars ++ " " ++ b vars ++ ")"

Then using the combinators from the other day:

type Term a = Elim (Lam :+: App) a type Expr = ForAll Term app_id_id :: Term a app_id_id = app (lam id) (lam id) -- for suitable definitions of app and lam a la the a la Carte paper. main = putStrLn . show $ safe app_id_id

Other algebra structures can be derived similarly.

March 26th, 2008 at 10:08 am

Looks like the syntax highlighter is cutting comments contents on the right (at least in firefox on win32).

Even so, the comment text is still there for selecting.

February 17th, 2012 at 10:21 pm

This web site seems to receive a little bit of comment spam, can I suggest you set up the spam free plugin – it has helped safeguard a selection of my personal web pages with great success