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.