There is a nice way of handling bound variables using non-uniform inductive types by considering terms as monads. Non-homogeneous inductive types are not widely known. Here is the Haskell definition of untyped lambda expressions.
> data Lambda a = Var a > | App (Lambda a) (Lambda a) > | Lambda (Lambda (Maybe a)) deriving (Eq, Show)
The idea is that the type variable a is the type of free
variables. Lambda abstraction introduces a new variable, so
Maybe a is used to add a new element to the type of
free variables.
Here are some examples of lambda expressions in this language.
> -- I = λx.x > i = Lambda (Var Nothing) > > -- K = λx.λy.x > k = Lambda (Lambda (Var (Just Nothing))) > > -- S = λf.λg.λx.f x (g x) > s = Lambda (Lambda (Lambda > (App (App (Var (Just (Just Nothing))) (Var Nothing)) > (App (Var (Just Nothing)) (Var Nothing)))))
If you read Nothing as “zero” and
Just as “successor” you can see this is a type of
De Bruijn notation.
Unfortunately this structure seems to violate what I said earlier about basic mathematical objects. Structural recursion seems inadequate for working with this object; it seems a more general recursion is necessary.
Finally, if you are wondering where the monad is, Var is
the return function and substitution is the bind function.