{--
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