{-

Towards a categorical treatment of variable binding.

The problem is to find a category with an endo-functor having an initial algebra which is recognisably the untyped lambda-calculus. A necessary criterion of recognisability is a definition of substitution using only structural recursion, meaning the universal properties of the initial algebra.

We start with the following Haskell code. {\small \begin{verbatim} data M x = Old x | New aM :: (x -> y) -> M x -> M y aM f m = case m of New -> New Old x -> Old (f x)

data E x = Var x | App (E x) (E x) | Abs (E (M x)) aE :: (x -> y) -> E x -> E y aE f e = case e of Var x -> Var (f x) App e1 e2 -> App (aE f e1) (aE f e2) Abs e -> Abs (aE (aM f) e)

lift :: (x -> E y) -> M x -> E (M y) lift phi m = case m of New -> Var New Old x -> aE Old (phi x)

sub :: E x -> (x -> E y) -> E y sub e phi = case e of Var x -> phi x App e1 e2 -> App (sub e1 phi) (sub e2 phi) Abs e -> Abs (sub e (lift phi))

subme :: E x -> M x -> E x subme e m = case m of { New -> e ; Old x -> Var x }

sub1 :: E (M x) -> E x -> E x sub1 e e' = sub e (subme e')

\end{verbatim} }

Anyone who has ever written functional programs to deal with lambda-calculus expressions in `de-Bruijn form', will have written something very like this code. If they wrote it in ML, they will shortly after have encountered a major brutality of ML's type system, that recursively defined names must be monomorphically typed. (See: Polymorphic Type Schemes and Recursive Definitions, Alan Mycroft, 1984 LNCS 167.) Haskell is slightly more accomodating. It allows polymorphic typing of such names, so long as you declare the types yourself. (If the type-declarations are commented out, the Haskell type-checker will reject the definitions.)

The program above can be written in constructive type-theory. The following, which needs revision and explanation, sketches one way to go about this, using the typechecker half. There is probably a theorem or two to prove that I've actually defined substitution correctly. (I believe that Hilbert, Ackermann, G\"odel, and numerous brilliant logicians actually had bugs in their definitions; and that the first logician to give a correct definition was Church, in his book `Mathematical Logic'. So maybe I shouldn't assume that my definition is correct!

-}


  Maybe ( X : Set ) {-  The `successor' of a set -}
  = data { $new, $old ( x : X ) } 
  : Set

,
  MaybeA ( X : Set, Y : Set, f : ( x : X )-> Y )
  = \ mx -> case mx of { $new  -> $new, $old x -> $old (f x) }
  : ( x : Maybe X )-> Maybe Y

,
  MaybeUnit ( X : Set )
  = \ x -> $old x
  : ( x : X )-> Maybe X

,
  MaybeBind ( X : Set, Y : Set, f : ( x : X )-> Maybe Y )
  = \ mx -> case mx of { $new  -> $new, $old x -> f x }
  : ( x : Maybe X )-> Maybe Y

{-

\newpage

-}

,
  FamSet   {-  A set-indexed family of sets -}
  = sig { U : Set, T : Pow U }
  : Type

, {-  The successor of a FamSet (not used) -}
  SUCC ( UT : FamSet )
  = struct {
      U = Maybe UT.U
    , T = \ u -> case u of { $new  -> UT.U, $old x -> UT.T x }
    }
  : FamSet
{-

%\newpage

-}

, {-  Closure of a family under Maybe -}
  Closure ( UT : FamSet ) 
  = let { 
      U   = UT.U : Set
    , T   = UT.T : Pow U 
    , U'  = data { $0 ( u : U ), $S ( p : U' ) } : Set
    , T'  = \ u' -> case u' of { $0 u -> T u
                               , $S p -> Maybe (T' p) } 
          : Pow U'
    } in
    struct { U = U', T = T' }
  : FamSet
{-

\newpage

-}

,
  Experiment1 ( UT : FamSet )
  = let 
    {
{-

-}

      UT' = Closure UT : FamSet
    ,
      I = UT'.U : Set   
    , 
      T = UT'.T : Pow I 
    , 
{-  We can make I into a category -}
      I_Arrow ( i : I, j : I )
      = ( x : T i )-> T j
      : Set

{-  Some properties of `maybe' re-expressed using the T-predicate -}
{-  `Maybe' is a kind of successor operator, hence letter `S'. -}
    , 
      S_Arrows( i : I, j : I )
      = MaybeA (T i) (T j) 
      : ( f : I_Arrow i j )-> I_Arrow ($S i) ($S j)
    , 
      S_Unit( i : I )
      = MaybeUnit (T i) 
      : I_Arrow i ($S i)
    ,
      S_Bind( i : I, j : I )
      = MaybeBind (T i) (T j) 
      : ( f : I_Arrow i ($S j) )-> I_Arrow ($S i) ($S j)
    , 
{-  The category we are looking for -}
{-  Since I is a category, we have some kind of pre-sheaves over I -}

      Obj = Pow I : Type  
    ,
      Arr = \ X Y -> 
            ( i : I )->
            ( x : X i )-> Y i
          : (X : Obj, Y : Obj )-> Set

{-  The endo-functor we are looking for -}

    , {-  On objects -}
      Phi = \ X i -> 
            data { $Var' ( x : T i )
                 , $App' ( f : X i, a : X i )
                 , $Abs' ( b : X ($S i) )
                 }
          : ( X : Obj )-> Obj 

    , {-  On arrows -}
      PhiA = \ X Y f -> 
             \ i x' -> 
             case x' of 
             { $Var' x    -> $Var' x
             , $App' f1 a -> $App' (f i f1) (f i a)
             , $Abs' b    -> $Abs' (f ($S i) b)
             }
           : ( X : Obj, Y : Obj, f : Arr X Y )->
             Arr (Phi X) (Phi Y)
    , 
      Phi_Init  {-  This causes technical problems with half -}
      = let { X = Phi X : Obj } in X 
      : Obj
    ,
      E  {-  A work-around. The object of the initial algebra for Phi. -}
      = \ i -> 
        data { $Var ( v : T i )
             , $App ( f : E i, a : E i)
             , $Abs ( b : E ($S i)) 
             } 
      : Obj
    , 
      E2PhiE ( i : I )  {-  Another part of the work around. -}
      = \ x -> case x of { $Var v   -> $Var' v
                         , $App f a -> $App' f a
                         , $Abs b   -> $Abs' b }
      : ( x : E i ) -> Phi E i

    , 
      {-  The initial algebra's structure map, if that's the right jargon -}
      Phi_InitA 
      = \ E' e' ->
        \ i x ->
        e' i  
        (PhiA E E' (Phi_InitA E' e') i (E2PhiE i x)) 
        {-

-}

      : ( E' : Obj, e' : Arr (Phi E') E' )->
        Arr E E' 

    , 
      {-  A functorial property of E. Should use structure map -} 
      lift ( i : I, e : E i )
      = \ j m ->
        case e of 
        { $Var v   -> $Var (m v)
        , $App f a -> $App (lift i f j m) (lift i a j m)
        , $Abs b   -> $Abs (lift ($S i) b ($S j) (S_Arrows i j m))
        }
      : ( j : I, m : I_Arrow i j )-> E j
    , 
      up
      = \ i x ->
        lift i x ($S i) (S_Unit i) 
      : ( i : I, x : E i )-> E ($S i)
    , 
      up1 ( i : I, j : I, m : ( x : T i )-> E j )
      = \ x ->
        case x of { $new    -> $Var $new, $old x1 -> up j (m x1) }
      : ( x : T ($S i) )-> E ($S j)

{-  The substitution function. Should use structure map -}
    , 
      sub ( i : I, e : E i )
      = \ j phi->
        case e of 
        { $Var v   -> phi v
        , $App f a -> $App (sub i f j phi) (sub i a j phi)
        , $Abs b   -> $Abs (sub ($S i) b ($S j) (up1 i j phi))
        }
      : ( j : I, phi : ( t : T i )-> E j )-> E j
    ,
      E' ( i : I )
      = ( j : I, phi : ( t : T i )-> E j )-> E j
      : Set
    , 
      E'A ( i : I, i' : I, m : I_Arrow i i', e' : E' i)
      = \ j phi -> e' j ( \ t -> phi (m t) )
      : E' i'
{-

\newpage

-}

    } in 
    {-  some debris from testing the above -}
    theory 
    { I_term ( i : I ) 
             = $Abs ($Var $new) 
             : E i
    , K_term ( i : I )
             = $Abs ($Abs ($Var ($old $new))) 
             : E i
    , S_term ( i : I )
             = $Abs ($Abs ($Abs 
                    ($App ($App ($Var ($old ($old $new))) 
                                ($Var $new))
                          ($App ($Var ($old $new)) 
                                ($Var $new))))) 
             : E i
    , M_term ( i : I )
             = $Abs ($App ($Var ($old $new)) ($Var ($old $new))) 
             : E ($S i)
    , test   ( i : I )
             = sub ($S i) (M_term i)  i 
               ( \ t -> case t of { $new  -> I_term i
                                  , $old x -> $Var x
                                  } )
             : E i
    }
  : Theory