***********************************************************************
* A Denotational Semantics Interpreter for the Lambda Calculus,       *
* from Chapter 10 of Reynolds.                                        *
***********************************************************************

Written by Paul Hudak.

> module LCInterpreter where

SYNTAX
======

> data Exp = Var String      -- variables
>          | App Exp Exp     -- applications
>          | Lam String Exp  -- abstractions
>      deriving (Eq, Show)

SEMANTIC DOMAINS
================

Reynolds defines a domain isomorphism:

Dinf ~ (Dinf -> Dinf)

with the pair of injection/projection functions:

phi :: Dinf -> (Dinf -> Dinf)
psi :: (Dinf -> Dinf) -> Dinf

He treats the domain very abstractly, and claims that its construction
is beyond the scope of the text.

However, suppose we wish to to prototype the denotational semantics in
Haskell?  How do we construct a datatype corresponding to Dinf?

We can get at an answer by asking a more fundamental question: what is
the meaning of a term in the lambda calculus?  From everything
discussed about reduction semantics, it seems that the operational
meaning of a term is either a term in normal form, or no term at all
in the case of divergence.  So let's try to mimick that idea by
creating a Haskell datatype for normal forms.  Remember that a normal
form is a lambda term with no beta redexes.  This leads to:

> data Dinf   = NoBeta NoBeta
>             | Fn (Dinf -> Dinf)
>
> data NoBeta = Vr String
>             | Ap NoBeta Dinf

Note the mutual recursive nature of these data types.  (Note also that
this solution is reminiscent of higher-order abstract syntax.)

Note also that a purely syntactic version of normal forms can be
defined as follows:

data NF = NoLam NoLam
        | Lm String NF

data NoLam = Vr String
           | App NoLam NF

We can define the pair of injection and projection functions on Dinf,
namely phi and psi, as follows:

> phi :: Dinf -> (Dinf -> Dinf)
> phi (NoBeta nb) = \d -> NoBeta (Ap nb d)
> phi (Fn f)     = f
>
> psi :: (Dinf -> Dinf) -> Dinf
> psi = Fn

phi and psi are "almost" inverses.  Everything works fine in this
direction:

  phi . psi = id:
  phi (psi f) = phi (Fn f) = f

In the other direction everything works fine with functions:

  psi . phi = id:
  psi (phi (Fn f)) = psi f = Fn f

but with NoBeta's we get the following:

  psi (phi (NoBeta nb)) 
  = psi (\d -> NoBeta (Ap nb d))
  = Fn (\d -> NoBeta (Ap nb d))
  = Fn (NoBeta . Ap nb)

This is not completely satisfactory, but makes sense intuitively, in
that the equivalence of (NoBeta nb) and (Fn (NoBeta . Ap nb)) is a
kind of eta-conversion.  (The fact that these are distinguished in
Dinf will mean that eta-conversion is not sound in the semantics.)

ENVIRONMENTS
============

> type Env = String -> Dinf
>
> extend :: Env -> String -> Dinf -> Env
> extend eta v d v' = if v == v' then d else eta v'

DENOTATIONAL SEMANTICS
======================

With the above preliminaries, the denotational semantics is completely
straightforward and precisely mimicks that in the text:

> red :: Exp -> Env -> Dinf
>
> red (Var s) eta     = eta s
> red (App e0 e1) eta = phi (red e0 eta) (red e1 eta)
> red (Lam v e) eta   = psi (\x -> red e (extend eta v x))

PRINTER
=======

The function "red" is essentially a normal-order lambda calculus
reducer, but is based on the denotational semantics rather than the
reduction semantics.  In order to display the result, we have to
figure out how to display values in Dinf.  The tricky part is
"reconstructing" lambda terms from values in (Dinf -> Dinf).  The
following function achieves that by passing a "fresh" name supply
around from which new variables can be created.  (The variable supply
should not include any free variables in the term being shown, but
here I have been lazy and left that part out.)

> vars :: [String]
> vars = ["a","b","c","d","e","f","g","h","i","j","k"]

> showDinf :: Dinf -> String
> showDinf d = fst (sdf d vars)

> sdf :: Dinf -> [String] -> (String, [String])
> sdf (NoBeta (Vr s))    vs = (s, vs)
> sdf (NoBeta (Ap nb d)) vs = 
>   let (snb, vs') = sdf (NoBeta nb) vs
>       (sd, vs'') = sdf d vs'
>   in ("(" ++ snb ++ " " ++ sd ++ ")", vs'')
> sdf (Fn f) (v:vs) = 
>   let (s, vs') = sdf (f (NoBeta (Vr v))) vs
>   in ("(\\" ++ v ++ "-> " ++ s ++ ")", vs')

TEST HARNESS
============

An initial environment that maps every variable to itself:

> eta0 :: Env
> eta0 v = NoBeta (Vr v)

A test function that reduces a term in the initial environment, then
"shows" the result:

> doit :: Exp -> IO ()
> doit e = putStrLn (showDinf (red e eta0))

EXAMPLES
========

A free variable:

> e0 = Var "x"

The identity combinator:

> e1 = Lam "x" (Var "x")

The self-application combinator:

> e2 = Lam "x" (App (Var "x") (Var "x"))

An application with a beta redex:

> e3 = App e1 e2

A test of name capture:

> e4 = App (Lam "x" (Lam "y" (Var "x"))) (Var "y")

A free variable under a lambda:

> e5 = Lam "x" (Var "y")

A redex under a lambda:

> e6 = Lam "z" e3

Note that eta contraction fails (precisely because phi and psi are
only "almost" inverses):

> e7 = Lam "x" (App (Var "y") (Var "x"))