{-
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
{
{- We want to assume we have a FamSet which is closed
under `maybe'. One way to do this is to assume we
have an arbitrary FamSet, and then work with its
closure under `maybe'.
-}
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))
{-#
(case x of
{ $Var v -> $Var v
, $App f a -> $App (Phi_InitA E' e' i f) (Phi_InitA E' e' i a)
, $Abs b -> $Abs (Phi_InitA E' e' ($S i) b)
})
-}
: ( 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