                                         premise
             peter 9094 Apr 19 17:57
            /home/peter/half/mu.half

April 19, 1999

   Exploring μ bindings 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 λ-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 μ 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 λ-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