{--
Exploring $\mu$ bindings \verb|1999-04-17 19:44:33|

These are some exercises, in which I define in a dependent type theory some datatypes for modelling metamathematically variable binding operators.

There may well be some silly errors...

--}

Pow  = \ S -> ( s : S )-> Set
: ( S : Type )-> Type,

Fam  = \ S -> sig { I : Set, g : ( i : I )-> S }
: ( S : Type )-> Type,

{--   disjoint union --}

plus = \ A B -> data { $i ( a : A ),$j ( b : B ) }
: ( A : Set, B : Set )-> Set,

{--   function space --}

imp  = \ A B -> ( a : A )-> B
: ( A : Set, B : Set )-> Set,

{--   empty set --}

emp  = data { }
: Set,

{--   maybe, option, whatever you want to call it --}

succ = \ A -> data { $0,$S ( a : A ) }
: ( A : Set )-> Set,

{--   empty family --}

Fam0 = struct { I = emp, g = \ i -> case i of { } }
: Fam Set,

{--   closing a family of sets under binary disjoint union --}

Clplus
= \ X ->
let {
U  = X.I
: Set,

T  = X.g
: Pow U,

U' = data { $g ( u : U ),$p ( a : U', b : U' ) }
: Set,

T' = \ u' ->
case u' of { $g u -> T u,$p a b -> plus (T' a) (T' b) }
: Pow U' }
in struct { I = U', g = T' }
: ( X : Fam Set )-> Fam Set,

{--   closing a family of sets under set-successor --}

Clsucc
= \ X ->
let {
U  = X.I
: Set,

T  = X.g
: Pow U,

U' = data { $g ( a : U ),$S ( a : U' ) }
: Set,

T' = \ u' -> case u' of { $g a -> T a,$S a -> succ (T' a) }
: Pow U' }
in struct { I = U', g = T' }
: ( X : Fam Set )-> Fam Set,

{--   closing a family of sets under both succ and disjoint union --}

Clplussucc
= \ X ->
let {
U  = X.I
: Set,

T  = X.g
: Pow U,

U' = data { $S ( u : U' ),$g ( u : U ), $p ( a : U', b : U' ) } : Set, T' = \ u' -> case u' of {$S u'  -> succ (T' u'),
$g u -> T u,$p a b -> plus (T' a) (T' b) }
: Pow U' }
in struct { I = U', g = T' }
: ( X : Fam Set )-> Fam Set,

{--   Expressions of the untyped $\lambda$-calculus. --}

experiment1
= \ X ->
theory {
X'    = Clsucc X
: Fam Set,

U     = X'.I
: Set,

T     = X'.g
: Pow U,

{--   now we are in the context of a family (U,T) closed under succ --}

E     = \ u ->
data {
$v ( t : T u ),$ap ( f : E u, a : E u ),
$ab ( body : E ($S u) ) }
: Pow U,

{--
that E is functorial. (Never mind about the equations for now.)

--}

mapE  = \ u u' f e ->
case e of {
$v t ->$v (f t),
$ap e1 e2 ->$ap (mapE u u' f e1) (mapE u u' f e2),
$ab body -> let { f' = \ a -> case a of {$0    -> $0,$S a1 -> $S (f a1) } : imp (T ($S u)) (T ($S u')) } in$ab (mapE ($S u) ($S u') f' body) }
: ( u  : U, u' : U, f  : imp (T u) (T u') )
-> imp (E u) (E u'),

{--   that E is a monad: unit --}

returnE
= \ u t -> $v t : ( u : U, t : T u )-> E u, {-- that E is a monad: bind --} bindE = \ u u' e f -> case e of {$v t -> f t,
$ap e1 e2 ->$ap (bindE u u' e1 f) (bindE u u' e2 f),
$ab body -> let { f' = \ a -> case a of {$0    -> $v$0,
$S a1 -> mapE u' ($S u') (\ x -> $S x) (f a1) } : imp (T ($S u)) (E ($S u')) } in$ab (bindE ($S u) ($S u') body f') }
: ( u  : U, u' : U, e  : E u, f  : imp (T u) (E u') )
-> E u' }
: ( X : Fam Set )-> Theory,

{--
A datatype of expressions built up from variables by a binary operator, and an operator $\mu$ that binds a family of variables simultaneously.

There is nothing of huge interest about these expressions - it is just an exercise, on the way to looking at more interesting datatypes.

--}

experiment2
= \ X ->
theory {
X'    = Clplus X
: Fam Set,

U     = X'.I
: Set,

T     = X'.g
: Pow U,

{--   now we are in the context of a family (U,T) closed under plus --}

E     = \ u ->
data {
$v ( t : T u ),$ap ( f : E u, a : E u ),
$mu ( u' : U, body : E ($p u' u) ) }
: Pow U,

{--   that E is functorial --}

mapE  = \ u u' f e ->
case e of {
$v t ->$v (f t),
$ap e1 e2 ->$ap (mapE u u' f e1) (mapE u u' f e2),
$mu bvt body -> let { f' = \ a -> case a of {$i a1 -> $i a1,$j b  -> $j (f b) } : imp (plus (T bvt) (T u)) (plus (T bvt) (T u')) } in$mu bvt
(mapE ($p bvt u) ($p bvt u') f' body) }
: ( u  : U, u' : U, f  : imp (T u) (T u') )
-> imp (E u) (E u'),

{--   that E is a monad: unit --}

returnE
= \ u t -> $v t : ( u : U, t : T u )-> E u, {-- that E is a monad: bind --} bindE = \ u u' e f -> case e of {$v t -> f t,
$ap e1 e2 ->$ap (bindE u u' e1 f) (bindE u u' e2 f),
$mu bvt body -> let { f' = \ a -> case a of {$i a1 -> $v ($i a1),
$j b -> mapE u' ($p bvt u')
(\ a1 -> $j a1) (f b) } : imp (T ($p bvt u)) (E ($p bvt u')) } in$mu bvt
(bindE ($p bvt u) ($p bvt u') body f') }
: ( u  : U, u' : U, e  : E u, f  : imp (T u) (E u') )
-> E u' }
: ( X : Fam Set )-> Theory,

{--

Something a little more serious. What I have in mind here is a datatype of expressions in which we have a non-empty family of mutually recursive equations. There is a distinguished element of the family which gives the output of the construction.

--}

experiment3
= \ X ->
theory {
X'    = Clplussucc X
: Fam Set,

U     = X'.I
: Set,

T     = X'.g
: Pow U,

{--
now we are in the context of a family $(U,T)$ closed under plus and succ

--}

E     = \ u ->
data {
$v ( t : T u ),$ap ( f : E u, a : E u ),
$mu ( u' : U, bodies : ( t : T ($S u') )-> E ($p ($S u') u) ) }
: Pow U,

{--   that E is functorial. (How to check the equations?) --}

mapE  = \ a b f e ->
case e of {
$v t ->$v (f t),
$ap e1 e2 ->$ap (mapE a b f e1) (mapE a b f e2),
$mu u' bodies -> let { f' = \ a1 -> case a1 of {$i a2 -> $i a2,$j b1 -> $j (f b1) } : imp (T ($p ($S u') a)) (T ($p ($S u') b)) } in$mu u'
(\ t ->
mapE ($p ($S u') a) ($p ($S u') b) f'
(bodies t)) }
: ( a : U, b : U, f : imp (T a) (T b) )-> imp (E a) (E b),

{--   that E is a monad: unit --}

returnE
= \ u t -> $v t : ( u : U, t : T u )-> E u, {-- that E is a monad: bind --} bindE = \ a b e f -> case e of {$v t -> f t,
$ap e1 e2 ->$ap (bindE a b e1 f) (bindE a b e2 f),
$mu u' bodies -> let { f' = \ a1 -> case a1 of {$i a2 -> $v ($i a2),
$j b1 -> mapE b ($p ($S u') b) (\ a2 ->$j a2) (f b1) }
: imp (T ($p ($S u') a))
(E ($p ($S u') b)) }
in $mu u' (\ t -> bindE ($p ($S u') a) ($p ($S u') b) (bodies t) f') } : ( u : U, u' : U, e : E u, f : imp (T u) (E u') ) -> E u' } : ( X : Fam Set )-> Theory, {-- An experiment motivated by trying to understand Thierry Coquand's approach to the treatment of names in inference systems. The datatype now is like the ordinary$\lambda$-calculus, but we add what Thierry calls instantiation'. I feel I must be missing the point. --} experiment4 = \ X -> theory { X' = Clsucc X : Fam Set, U = X'.I : Set, T = X'.g : Pow U, E = \ u -> data {$v  ( t : T u ),
$ap ( f : E u, a : E u ),$ab ( body : E ($S u) ),$instantiation
( u'  : U, e   : E u', rho : ( t : T u' )-> E u ) }
: Pow U,

{--   that E is functorial. (How to check the equations?) --}

mapE  = \ a b f e ->
case e of {
$v t ->$v (f t),
$ap e1 e2 ->$ap (mapE a b f e1) (mapE a b f e2),
$ab body -> let { f' = \ a1 -> case a1 of {$0    -> $0,$S a2 -> $S (f a2) } : imp (T ($S a)) (T ($S b)) } in$ab (mapE ($S a) ($S b) f' body),
$instantiation u' e1 rho ->$instantiation u' e1
(\ t -> mapE a b f (rho t)) }
: ( a : U, b : U, f : imp (T a) (T b) )-> imp (E a) (E b),

{--   that E is a monad: unit --}

returnE
= \ u t -> $v t : ( u : U, t : T u )-> E u, {-- I've the feeling there is something idiotic here --} bindE = \ a b e f -> case e of {$v t -> f t,
$ap e1 e2 ->$ap (bindE a b e1 f) (bindE a b e2 f),
$ab body -> let { f' = \ a1 -> case a1 of {$0    -> $v$0,
$S a2 -> mapE b ($S b) (\ a3 -> $S a3) (f a2) } : imp (T ($S a)) (E ($S b)) } in$ab (bindE ($S a) ($S b) body f'),
$instantiation u' e1 rho ->$instantiation u' e1
(\ t -> bindE a b (rho t) f) }
: ( u  : U, u' : U, e  : E u, f  : imp (T u) (E u') )
-> E u' }
: ( X : Fam Set )-> Theory

`