--- How to bind a variable.

The following is some Haskell code in which it is shown by way of an
example how substitution in the presence of variable binding operators
can be defined using only structural recursion.  The example is the
untyped $\lambda$-calculus.

The constructions here are in my opinion very simple.  They are
strikingly close to what is formalised in Pierre Lescanne's
$\lambda\upsilon$ calculus\footnote{See: |
http://www.ens-lyon.fr/\~{}plescann/|} of explicit substitutions. 

Identifying bound variables is only one of the uses to which names are
put in formal systems such as programming languages, specification
languages, or inference systems.  Others are (thinking of inference
systems) names for rules, for premises, for collections of rules,
labels of one kind or other, place-holders, and what are nowadays
sometimes called `holes' in incomplete proofs, or other formal
contexts.  Turning to specification languages, there are state
variables (both free and bound).  All of these are problematic in some
way.  Bound variables were `invented' by Frege over a century ago, and
in some ways we have still to understand thoroughly what he gave us.
Draw your own conclusions!

Postscript: Conor McBride has just |(1999-05-08 10:32:36)| just shown
me a paper `de Bruijn notation as a nested datatypes' by Richard Bird
and Ross Paterson, which contains much the same code modulo
`$\alpha$-conversion'. It is to be published in JFP, and is dated 1998.
Conor also showed me a paper by Thorsten Altenkirch and Bernard Reus
that contains similar ideas (taken much further), and a very interesting
treatment of \emph{typed} calculi. 

> module Lambda_calculus where 
> import Char

-- Preliminaries

The type constructor |S| is really the prelude function |Maybe|,
which has constructors |New| and |Old|.  I define it explicitly for people who
don't know the Haskell prelude.  It arises also in
Martin-L\"of's type theory: see Nordstr\"om, Petersson and Smith,
Programming in Martin-L\"of's Type Theory, pp 103-104. 

> data S x = Top | Pop x deriving (Show, Eq)

The following function |eS| is the basic combinator for defining functions
from types of form |S|.

> eS :: (x -> y) -> y -> S x -> y
> eS f y m = case m of Pop x -> f x
>                      Top   -> y

It seems worth introducing some mnemonic notation.

> infixl 1 |>  -- very low precedence, below (.)
> (|>) = eS    -- f |> d = eS f d : d is a "default".

Using it, we can make |S| into a functor, and a monad.
(It isn't used that |S| is a monad.)

> instance Functor S where
>   fmap f   = Pop . f |> Top  -- (>>= (return . f))
> instance Monad S where
>   return  = Pop              -- unit
>   m >>= f = (f |> Top) m     -- bind

[ In Haskell, |return| is the unit of the monad, and |>>=| is
the bind operation. ]

-- The lambda expression datatype functor.

Now we introduce a datatype constructor for lambda-expressions,
de-Bruijn style. The parameter of the type constructor is a type of
names for variables that may occur free in the lambda-expression.

> infixl 8 :@: 
> data L x = Var x 
>          | L x :@: L x 
>          | Abs (L (S x))            
>          deriving (Show, Eq)  -- convenient for experimentation.

Now we define renaming, by structural recursion. For the definition to
type-check, we need polymorphic recursion, which luckily for us is
supported in Haskell.  This means that as long as we declare the
polymorphic type, the various occurrences of the function can have
different types, as long as they are instances of the polymorphic type. 

> rename :: L x -> (x -> y) -> L y
> e `rename` f = case e of 
>                     Var x      -> Var (f x)
>                     e1 :@: e2  -> e1 `rename` f :@: e2 `rename` f
>                     Abs bd     -> Abs (bd `rename` (fmap f))

[In Haskell, |a `foo` b| is equivalent to |(foo a b)|.  Putting
backquotes fore and aft is just a way of turning |foo| into an infix
operator.]

Note that the `fmap' in the last line refers to the functor |S|. (The
de-overloading of `fmap' to its different definitions at different
types is figured out by the Haskell typechecker.)

Like any other sum-of-products positive datatype constructor, |L| is a
functor.  This means we can use `map' to refer to it in Haskell.  

> instance Functor L where  
>   f `fmap` e = e `rename` f 

In fact, as shown in the next section, it is a monad, so we can also
use do notation and other confectionary in the Haskell sweet-shop. 

-- Simultaneous substitution, monad structure.

Now we define simultaneous substitution, by structural recursion.  A
simultaneous substitution is a function from variable names to
substituents, perhaps with respect to a different name space. Again,
we need polymorphic recursion.

> subst :: L x -> (x -> L y) -> L y
> e `subst` f = 
>   case e of Var x      -> f x
>             e1 :@: e2  -> e1 `subst` f :@: e2 `subst` f
>             Abs bd     -> Abs (bd `subst` f') 
>                           where f' = (`rename` Pop) . f 
>                                      |> Var Top

[ In Haskell, |f . g| means composition, with |g| first, then |f|. ]

Like any other `leafy' datatype constructor\footnote{See Bird and de
Moor, Algebra of Programming, exercise 2.40.  `Leafy' is my own
metaphor.}, |L| is a monad.  The bind operator is simultaneous
substitution.

> instance Monad L where
>   return = Var 
>   (>>=)  = subst

-- Single point substitution, an application.

Now we can define the usual `one-variable' substitution.  Because |L|
is a monad, Haskell's `do' notation is available, and we may as well
use it.

> subst1 :: L (S x) -> L x -> L x
> subst1 c e = do { x <- c ; (Var |> e) x }             --  c >>= eS Var e

The first argument of |subst1| is an expression containing a
distinguished variable, and the second argument, which does not
contain that variable (nor any variable bound in the first argument)
is substituted for this variable.

As an application for |subst1| we define a partial function which
reduces lambda-calculus expressions to weak head normal form. (In 4
lines of code, and 2 superfluous type statements!)

> evL :: L a -> L a
> evL z = case z of e1 :@: e2  -> app (evL e1) e2       
>                   _          -> z 

The functiom |app| is a helper for |evL|, and mutually recursive with it. 

> app :: L a -> L a -> L a
> app z = case z of Abs e      -> evL . subst1 e 
>                   _          -> (z  :@:)

Unfortunately, de Bruijn machinery is too costly for use in a
practical reduction machine. Or is it? 

-- Continuation transform (call by name/value)

Another illustration of recursion over |L| : the call by name/value
continuation transforms. (If I have transcribed them correctly...)

> cbn, cbv :: L x -> L x
> cbn m = case m of 
>    Var x     -> Abs (Var Top :@: Var (Pop x))
>    Abs e     -> Abs (Var Top :@: Abs (lift (cbn e)))
>    e1 :@: e2 -> Abs (lift (cbn e1) 
>                      :@: Abs (lift (lift (cbn e2)) 
>                                :@: Abs (Var (Pop Top)
>                                         :@: (Var Top)
>                                         :@: (Var (Pop (Pop Top))))))
> cbv m = case m of 
>    Var x     -> Abs (Var Top :@: Var (Pop x))
>    Abs e     -> Abs (Var Top :@: Abs (lift (cbv e)))
>    e1 :@: e2 -> Abs (lift (cbv e2) 
>                      :@: Abs (lift (lift (cbv e1)) 
>                                :@: Abs (Var Top 
>                                         :@: (Var (Pop Top)) 
>                                         :@: (Var (Pop (Pop Top))))))
> lift = (`rename` Pop)

-- Normal terms.

We can also define a type of normal terms. (I learnt this from
Marcello Fiore.)

> data Norm x = Ab (Norm (S x)) 
>             | Ap x [Norm x] 
>             deriving (Show, Eq)

This gives us a functor.

> instance Functor Norm where fmap = nrn
> nrn :: (x -> y) -> Norm x -> Norm y
> nrn f (Ab b)    = Ab (nrn f' b) where f' = fmap f 
> nrn f (Ap x bs) = Ap (f x) [ nrn f b | b <- bs ]

It does not give us a monad.  Substitution of normal terms in normal
terms can give rise to non-normal terms.  To find a monad here we
would need to restrict expressions to a suitable type system, and
prove (essentially) cut elimination.  I haven't done this; there's
quite a lot to figure out.

A normal expression is either an abstraction whose body is normal, or
of the form of a variable applied to a `spine' of normal
arguments. Here, the list constructor |[x]| is used for a spine.  So a
variable with name x has the form |Ap x []|.  Normal expressions can
be embedded among the ordinary ones as follows:

> emb :: Norm x -> L x
> emb (Ap x ns) = foldl (\s -> (s :@:) . emb) (Var x) ns
> emb (Ab e)    = Abs (emb e)

Here's a definition of substitution which probably terminates when
the expressions are well typed. 

> sb :: Norm x -> (x -> Norm y) -> Norm y
> ap :: Norm x -> [Norm x] -> Norm x
> sb (Ap x bs) f   = f x `ap` [sb b f | b <- bs]
> sb (Ab b) f      = Ab (sb b f')
>                    where f' Top = Ap Top []          
>                          f' (Pop x) = fmap Pop (f x)
> ap (Ap y cs) ds  = Ap y (cs ++ ds)
> ap (Ab c) (b:bs) = sb c f' `ap` bs 
>                    where f' Top = b 
>                          f' (Pop x) = Ap x []
> ap e []          = e

-- Categories and stuff

I haven't got a reliable description of what is going on
categorically.  However, I know some gentlemen who do: Marcello Fiore,
Danieli Turi, and Gordon Plotkin.  You should read their paper: |<a
href="http://www.dcs.ed.ac.uk/home/dt/abstractsyn.ps">Abstract Syntax
and Variable Binding</a>| The essence of it is that we have here an
initial algebra for a particular endofunctor in the presheaf category
over a certain category of contexts which in this case we can take to
be the category of finite cardinals (and all functions).  Moreover, in
the case of the datatype of lambda-terms, we have what seems to be the
simplest possible non-trivial example in which the endofunctor makes
use of the structure of the category of contexts: here that it is
closed under the `successor' operation |S|.

The categorical perspective provides (they tell me) a setting for a
more delicate analysis of variable binding, including forms of linear
abstraction.  It also suggests ways of modelling the syntax of typed
binding constructs.  It may put in our hands powerful new kinds of
data structure.

-- Parsing of L.

At one time I thought it was tricky to write a parser for L, but it is
really quite straightforward.  I would like to thank Lennart
Augustsonn for sending me once some spectacularly clever code that
almost worked, at a point when I thought it impossible.  However his
code turned out to be unnecessary, so I have no excuse for showing it
to you, and you will have to do with this miserable hack instead.

Example syntax

> k_str = "\\x y ->x"
> s_str = "\\f g x-> f x (g x)"

To parse a string |str|, returning maybe an expression, evaluate
in the interpreter |parseL str|.

> parseL :: String -> Maybe (L String)
> parseL s = case [e | (e, "") <- expr s ] of
>            [e] -> Just e
>            _   -> Nothing

This is just a quick hack, using list comprehensions, and `list of
successes' parsers.  Probably one shouldn't read it, even if one could.

> expr s = 
>   applicative s ++ abstraction s
>   where
>    ident s = 
>       [ (Var i, s') | (i, s') <- lex s, all isAlpha i, i /= "" ]
>    bracketed s = 
>       [ (e, s''') | ("(", s')   <- lex s,
>                     (e , s'')   <- expr s',
>                     (")", s''') <- lex s'' ]
>    atomic s = bracketed s ++ ident s
>    applicative s = 
>       [ (foldl (:@:) e es, s'') | 
>                     (e, s')      <- atomic s, 
>                     (es, s'')    <- rep atomic s'] 
>    abstraction s = 
>       [ (foldr abs e is, s'''') | 
>                     ("\\", s')   <- lex s,
>                     (is, s'')    <- rep ident s', 
>                     ("->", s''') <- lex s'',
>                     (e, s'''')   <- expr s''']
>       where abs (Var i) = Abs . fmap (\ x -> if x == i then Top else Pop x) 
>    rep p s = [ (x:xs, s'') | (x, s') <- p s, (xs, s'') <- rep p s']
>              ++ [([],s)]

-- What pretty printing problem?

De Bruijn's representation for bound variables is fine for computers,
but lousy for humans.  (One can imagine a Turing test along these
lines..)  Can we `decorate' bound variables with the names which Joe
User gives them when he writes down an expression to be parsed, so
that we can use the same names when the expression is printed?  Yes.
Here is how, recycled from the code above, by good old cut and paste.

Let us change |S| a little.

> data S' x = Top' String     -- decoration
>           | Pop' x 
>           deriving Show

(This could be parameterised with respect to String.)

> eS' :: (x -> y) -> (String -> y) -> S' x -> y
> eS' f g m = case m of Top' str -> g str
>                       Pop' x   -> f x
> instance Functor S' 
>   where fmap f = eS' (Pop' . f) Top'
> instance Monad S' 
>   where return   = Pop' 
>         m >>= f  = eS' f Top' m

> data L' x = Var' x 
>           | App' (L' x) (L' x) 
>           | Abs' (L' (S' x))    deriving Show

> mapL' :: (x -> x') -> L' x -> L' x'
> mapL' f m = case m of 
>               Var' x      -> Var' (f x)
>               App' e1 e2  -> App' (mapL' f e1) (mapL' f e2) 
>               Abs' bd     -> Abs' (mapL' (fmap f) bd) 

> instance Functor L' where fmap = mapL'

> bind' :: L' x -> (x -> L' y) -> L' y
> bind' l f = case l of 
>               Var' x     -> f x
>               App' e1 e2 -> App' (bind' e1 f) (bind' e2 f) 
>               Abs' bd    -> Abs' (bind' bd f')
>                             where f' = eS' (fmap Pop' . f) 
>                                            (Var' . Top')

> instance Monad L' 
>   where return = Var'
>         (>>=) = bind'


> parseL' :: String -> Maybe (L' String)
> parseL' s = case [e | (e, "") <- expr' s ] of
>              [e] -> Just e
>              _ -> Nothing

> expr' s = 
>   applicative s ++ abstraction s 
>   where
>    ident s = 
>       [ (Var' i, s') |
>         (i, s') <- lex s, all isAlpha i && i /= "" ]
>    bracketed s = 
>       [ (e, s''') | 
>         ("(", s')    <- lex s,
>         (e , s'')    <- expr' s',
>         (")", s''')  <- lex s'' ]
>    atomic s = bracketed s ++ ident s
>    applicative s = 
>       [ (foldl App' e es, s'')  |
>         (e, s')      <- atomic s, 
>         (es, s'')    <- rep atomic s' ] 
>    abstraction s = 
>       [ (foldr abs e is, s'''') | 
>         ("\\", s')   <- lex s,
>         (is, s'')    <- rep ident s', 
>         ("->", s''') <- lex s'',
>         (e, s'''')   <- expr' s''' ]
>       where abs (Var' i) = Abs' . fmap (\ x -> if x == i then Top' i 
>                                                          else Pop' x) 
>    rep p s = 
>       [ (x:xs, s'') | 
>         (x, s')      <- p s, 
>         (xs, s'')    <- rep p s' ]
>       ++ [([],s)]


That seems to work.  Is there any real problem here?  

-- Conclusion

The pattern of recursion involved in the definition of |L| is
interesting, or at least unusual.  Usually the recursion is at 
the level of types; here it is at the level of types to types.

All we assume about the domain of |L| is that it is closed under |S|.
We could have a dependent type system, in which the arguments of |L|
are data-values, representing types via a decoding function. 

It is interesting that so many of the functions require polymorphic
recursion.  My feeling is that in order to deal properly with subtle
forms of recursion, we `really' need a dependent type system.  (To
make this case, I have to look at the general form of the recursion
combinator and its type, and explore instances `on the edge' --
admittedly, there are none above.  But if one leans more heavily on
Haskell's polymorphic recursion, examples can probably be found where
it breaks.)

- Some expressions for experimenting with

> v0 = Var n0
> v1 = Var n1
> v2 = Var n2

> n0 = Top
> n1 = Pop Top
> n2 = Pop (Pop Top)
> var n = Ap n []

> b_term    = Abs (Abs (Abs (v2 :@: (v1 :@: v0))))
> c_term    = Abs (Abs (Abs (v2 :@: v0 :@: v1)))
> w_term    = Abs (Abs (v1 :@: v0 :@: v0))
> k_term    = Abs (Abs v1)
> i_term    = Abs v0
> s_term    = Abs (Abs (Abs (v2 :@: v0 :@: (v1 :@: v0))))
> y_term    = Abs (x :@: x)  where x = Abs (v1 :@: (v0 :@: v0))
> sap       = Abs (v0 :@: v0)
> dont_evaluate_me = sap :@: sap
> fix_term = Abs (let x = v0 :@: x in x) 
> fix_term, w_term, i_term, k_term, s_term, c_term :: L String