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