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.

I haven't got a description of what is going on categorically.
However, the right-hand side of the definition of `L' below is
essentially a endofunctor on a certain category of set-valued
functions, and `L' is its initial algebra.  The domain of these
functions can be any family of sets closed under `Maybe' - for example
the von-Neumann natural numbers. The question of picking the right
morphisms to make the members of this family into the objects of a
category (and L into the initial object for a functor on the
presheaves over that category) is a bit too abstruse for me at the
moment.  I leave it as an exercise for the categorically obsessed. 

The simple constructions here are strikingly close to the notions
formalised in Pierre Lescanne's $\lambda\upsilon$ calculus of explicit
substitutions. See:
|<a href="http://www.ens-lyon.fr/~plescann/"><a/>|.

> module Lambda_calculus (L(Var,App,Abs), 
>        i_term,b_term,c_term,w_term,k_term,s_term,y_term,fix_term) where

A data-type for lambda-expressions, de-Bruijn style. The parameter is
a type of names for variables.

> data L x = Var x 
>          | App (L x) (L x) 
>          | Abs (L (Maybe x))
>            deriving (Show,Read)  -- just for testing

Like any other sum-of-products positive data-type, L is a functor in
the sense of acting on arrows.  To define this, we need polymorphic
recursion, as supported in Haskell.  Basically, the functor renames
free variables.

> instance Functor L where  map = mL

> mL :: (x -> y) -> L x -> L y   -- need an explicit type assertion
> mL f z = case z of 
>               Var x     -> Var (f x)
>               App e1 e2 -> App (mL f e1) (mL f e2) 
>               Abs e     -> Abs (mL f' e) 
>                        where -- note how bound variables are protected
>                              f'  = map f -- Maybe is itself a functor
 
Like any other leafy data-type, L is a monad.  The bind operator is
simultaneous substitution.  

(`Leafy data type': |f x = mu (\ y -> x + g y )|. See Bird and de Moor,
Algebra of Programming, exercise 2.40.) 

> instance Monad L where
>   return a = Var a
>   e >>= f  = case e of 
>                Var x -> f x
>                App e1 e2 -> App (e1 >>= f) (e2 >>= f)
>                Abs e -> Abs (e >>= f') 
>                         where -- note how capture of frees is avoided
>                               f' w = case w of Nothing -> Var Nothing
>                                                Just x  -> map Just (f x)

Conventional one-point substitution.  As we have a monad, we
can exploit Haskell's "do" notation. 

> subst1 :: L (Maybe x) -> L x -> L x
> subst1 c e = do z <- c
>                 case z of Nothing -> e      
>                           Just x -> Var x

- An application

We define a partial function which reduces 
lambda-calculus expressions to WHNF. (In 4 lines of code!)

A helper.

> app z = case z of Abs e -> evL . subst1 e 
>                   _     -> App z 

Compute WHNF

> evL z = case z of App e1 e2  -> app (evL e1) e2       
>                   _          -> z 

Unfortunately, de Bruijn machinery seems too costly for use in a
practical reduction machine.

- Some expressions for experimenting with

> v0 = Var Nothing 
> v1 = Var (Just Nothing)
> v2 = Var (Just (Just Nothing))

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