HOAS evaluation

This literatare Haskell program demonstrates how Higher Order Abstract Syntax (HOAS)
allows for very simple step-wise evaluation in the untyped lambda calculus.

> module HOAS where
> import Text.PrettyPrint.HughesPJ(Doc, renderStyle, style, text, (<>), (<+>), parens)
> import Data.List(unfoldr)
> import Control.Monad(mplus)
> import Data.Maybe(Maybe,fromJust)

A term is either an abstraction, represented by a Haskell function binding a variable identifier,
an application, or a bound variable identifier.

> data HOAS = Lam (HOAS -> HOAS) | App HOAS HOAS | Var Char

Var is not used for only for printing terms, not for representing them.
The identity function is simply represented as

> i :: HOAS
> i = Lam(\f-> f)

and the two basis functions in combinatory logic as

> k :: HOAS
> k = Lam(\x-> Lam(\y-> x))
> s :: HOAS
> s = Lam(\x-> Lam(\y-> Lam(\z-> (x `App` z) `App` (y `App` z))))

Evalution to normal form is a simple matter
of evaluating the body in an abstraction, both the function and argument
in an application, and applying the representing Haskell function when
the former evaluates to an abstraction, which will perform substitution
without all the usual headaches, like free variable capture, of a classical representation.

> nf :: HOAS -> HOAS
> nf (Lam f)   = Lam (nf . f)
> nf (App f a) = case nf f of { Lam g -> g; g -> App g } $ nf a
> nf x         = x

Performing individual beta reduction steps is almost as easy,
only complicated by the need to determine if an abstraction body has a redex:

> step :: HOAS -> Maybe HOAS
> step (App (Lam f) a) = Just $ f a
> step (App f       a) = fmap (`App` a) (step f) `mplus` fmap (f `App`) (step a)
> step (Lam f)         = step (f (Var undefined)) >> Just (Lam (fromJust . step . f))
> step x               = Nothing

Combining steps by unfolding

> steps :: HOAS -> [HOAS]
> steps = unfoldr (fmap (\x->(x,x)) . step)

gives us an alternative way to derive normal forms as

> slownf :: HOAS -> HOAS
> slownf = last . steps

It remains to show off the fruits of our efforts with a pretty printer

> pp :: Int -> Char -> HOAS -> Doc
> pp _ g (Var   v) = text $ [v]
> pp p g (Lam   e) = (if p>0 then parens else id) $ text ['\\',g,' '] <> pp 0 (succ g) (e (Var g))
> pp p g (App f a) = (if p>1 then parens else id) $ pp 1 g f   <+> pp 2 g a

> instance Show HOAS where
>   show = renderStyle style . pp 0 'a'

Example reduction of predecessor of Church numeral one

> prd = Lam(\n->Lam(\f->Lam(\x->n`App`Lam(\g->Lam(\h->h`App`(g`App`f)))`App`Lam(\u->x)`App`i)))
> example1 = prd `App` i

Infinite reduction

> dbl = Lam (\x -> x `App` x)
> example2 = dbl `App` dbl

Ackermann

> ack = Lam(\n->n`App`Lam(\f->Lam(\m->f`App`(m`App`f`App`i)))`App`Lam(\m->Lam(\f->Lam(\x->f`App`(m`
App`f`App`x))))`App`n)
> two = Lam(\f->Lam(\x->f`App`(f`App`x)))
> example3 = ack `App` two

> showoff :: HOAS -> IO ()
> showoff = mapM_ print . steps

> main = showoff example3

The only downside is that variable names do not preserve identity between steps,
and only indicate binding depth.