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

The constructions here are in my opinion very simple. They are strikingly close to what is formalised in Pierre Lescanne’s λυ calculus^{1} 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 ‘α-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 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öf’s type theory: see Nordström, Petersson and Smith, Programming in Martin-Löf’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.

1See: http://www.ens-lyon.fr/~plescann/

    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^{2}, 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.

2See Bird and de Moor, Algebra of Programming, exercise 2.40. ‘Leafy’ is my own metaphor.

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