Non-homogeneous Inductive Types


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.


, ,

Russell O’Connor: contact me