Summer school 2008:Type safety for MinML with monadic effects

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.
Summer school 2008
Previous: Exercies 3


Type safety for MinML with monadic effects

Syntax / static semantics

Types:

tp : type.				%name tp T.
nat : tp.
arr : tp -> tp -> tp.
circle : tp -> tp.  %% called 'comp' in PFPL;
                    %% the lax modality is often rendered as a circle

Next, we define typed expressions (i.e., typing derivations). There are two syntactic classes: pure expressions, and possibly-effectful commands.

exp  : tp -> type.			%name exp E.  %postfix 1 exp.
command : tp -> type.			%name command M.  %postfix 1 command.

z : nat exp.
s : nat exp -> nat exp.
ifz : nat exp -> T exp -> (nat exp -> T exp) -> T exp.
fun : {T1:tp} {T2:tp} ((arr T1 T2) exp -> T1 exp -> T2 exp) -> (arr T1 T2) exp.
app : (arr T1 T2) exp -> T1 exp -> T2 exp.
comp : T command -> (circle T) exp.

return : T exp -> T command.
let    : (circle T) exp -> (T exp -> U command) -> U command.

Dynamic semantics / preservation

Values and final states

value : T exp -> type.			%name value Dval.
%mode value +E.

value/z : value z.
value/s : value (s E) <- value E.
value/fun : value (fun _ _ _).
value/comp : value (comp _).

final : T command -> type.                 %name final Dfin.
%mode final +M.

final/ret : final (return E)
	     <- value E.

Transition relation for expressions

step : T exp -> T exp -> type.		%name step Dstep.
%mode step +E1 -E2.

step/s
   : step (s E) (s E') <- step E E'.
step/ifz/arg
   : step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))
      <- step E E'.
step/ifz/z
   : step (ifz z E1 ([x] E2 x)) E1.
step/ifz/s
   : step (ifz (s E) E1 ([x] E2 x)) (E2 E)
      <- value E.
step/app/fun
   : step (app E1 E2) (app E1' E2)
      <- step E1 E1'.
step/app/arg
   : step (app E1 E2) (app E1 E2')
      <- value E1 <- step E2 E2'.
step/app/beta-v
   : step
      (app (fun T1 T2 ([f] [x] E f x)) E2)
      (E (fun T1 T2 ([f] [x] E f x)) E2)
      <- value E2.

Transition relation for commands

mstep : T command -> T command -> type.		%name mstep Dstep.
%mode mstep +E1 -E2.

mstep/ret : mstep (return E) (return E')
	     <- step E E'.
mstep/let-e : mstep (let E ([x] M x)) (let E' ([x] M x))
	       <- step E E'.
mstep/let-m : mstep (let (comp M1) ([x] M2 x)) (let (comp M1') ([x] M2 x))
	       <- mstep M1 M1'.
mstep/let-beta : mstep (let (comp (return E)) ([x] M x)) (M E)
		  <- final (return E).

Progress

The progress theorem for expressions does not require a corresponding theorem for commands, because commands are suspended inside expressions (comp M is always a value). We prove progress for expressions first, and for commands below.

Return sums

val-or-step : T exp -> type.		%name val-or-step Dvos.
vos/val : val-or-step E <- value E.
vos/step : val-or-step E <- step E _.

fin-or-mstep : T command -> type.       %name fin-or-mstep Dfos.
fos/fin : fin-or-mstep M <- final M.
fos/step : fin-or-mstep M <- mstep M _ .

Factoring lemmas

prog/s
   : val-or-step E -> val-or-step (s E) -> type.
%mode prog/s +Dvos1 -Dvos2.

- : prog/s
     (vos/step Dstep)
     (vos/step (step/s Dstep)).
- : prog/s
     (vos/val Dval)
     (vos/val (value/s Dval)).

%worlds () (prog/s _ _).
%total {} (prog/s _ _).

prog/ifz
   : val-or-step (E : nat exp)
      -> {E1} {E2} (step (ifz E E1 ([x] E2 x)) E')
      -> type.
%mode prog/ifz +E +E1 +E2 -Dstep.

- : prog/ifz (vos/step Dstep) _ _ (step/ifz/arg Dstep).
- : prog/ifz (vos/val value/z) _ _ step/ifz/z.
- : prog/ifz (vos/val (value/s Dval)) _ _ (step/ifz/s Dval).

%worlds () (prog/ifz _ _ _ _).
%total {} (prog/ifz _ _ _ _).

prog/app
   : val-or-step (E1 : (arr T2 T) exp)
      -> val-or-step (E2 : T2 exp)
      -> step (app E1 E2) E'
      -> type.
%mode prog/app +Dvos1 +Dvos2 -Dstep.

- : prog/app
     (vos/step Dstep1)
     _
     (step/app/fun Dstep1).

- : prog/app
     (vos/val Dval1)
     (vos/step Dstep2)
     (step/app/arg Dstep2 Dval1).

- : prog/app
     (vos/val Dval1)
     (vos/val Dval2)
     (step/app/beta-v Dval2).

%worlds () (prog/app _ _ _).
%total {} (prog/app _ _ _).

Progress for expressions

prog : {E : T exp} val-or-step E -> type. %name prog Dprog.
%mode prog +E -Dvos.

- : prog z (vos/val value/z).

- : prog (s E) Dvos'
     <- prog E Dvos
     <- prog/s Dvos Dvos'.

- : prog (ifz E E1 ([x] E2 x)) (vos/step Dstep)
     <- prog E Dvos
     <- prog/ifz Dvos _ _ Dstep.

- : prog (fun _ _ _) (vos/val value/fun).

- : prog (app E1 E2) (vos/step Dstep)
     <- prog E1 Dvos1
     <- prog E2 Dvos2
     <- prog/app Dvos1 Dvos2 Dstep.

- : prog (comp M) (vos/val value/comp).

%worlds () (prog _ _).
%total Dof (prog Dof _).

Factoring lemmas for commands

mprog/ret : val-or-step E -> fin-or-mstep (return E) -> type.
%mode mprog/ret +X1 -X2.

- : mprog/ret (vos/val Dval) (fos/fin (final/ret Dval)).
- : mprog/ret (vos/step Dstep) (fos/step (mstep/ret Dstep)).

%worlds () (mprog/ret _ _).
%total {} (mprog/ret _ _).

mprog/let-comp : fin-or-mstep (M1 : T command) -> {M2 : (T exp -> U command) } mstep (let (comp M1) M2) M' -> type.
%mode mprog/let-comp +X1 +X2 -X3.

- : mprog/let-comp 
     (fos/fin ((final/ret Dval) : final (return E))) 
     M2 
     ((mstep/let-beta (final/ret Dval)) : mstep (let (comp (return E)) M2) (M2 E)).

- : mprog/let-comp 
     (fos/step 
	(Dmstep : mstep M1 M1')
	)
     M2
     ((mstep/let-m Dmstep) : mstep (let (comp M1) M2) (let (comp M1') M2)).

%worlds () (mprog/let-comp _ _ _).
%total {} (mprog/let-comp _ _ _).

Progress for commands

The factoring lemma for let is is mutually recursive with the main theorem---when the let-bound expression is comp M, we need to recursively appeal to progress on M.

mprog/let : {E : (circle T) exp} val-or-step E -> {M : (T exp -> U command) } mstep (let E M) M' -> type.
%mode mprog/let +X1 +X2 +X3 -X4.

mprog : {M : T command} fin-or-mstep M -> type.
%mode mprog +M -Dfos.

%% mprog/let

- : mprog/let (comp M) (vos/val value/comp) _ Dmstep
     <- mprog M Dfos
     <- mprog/let-comp Dfos _ Dmstep.

- : mprog/let _ (vos/step Dstep) _ (mstep/let-e Dstep).

%% mprog

- : mprog (return E) Dfos
     <- prog E Dvos
     <- mprog/ret Dvos Dfos.  

- : mprog 
     (let (E : (circle T) exp)
	(M : (T exp -> U command)))
     (fos/step Dmstep)
     <- prog E (Dvos : val-or-step E)
     <- mprog/let E Dvos M (Dmstep : mstep (let E M) M').

%worlds () (mprog _ _) (mprog/let _ _ _ _).
%total (M E) (mprog M _) (mprog/let E _ _ _).

Because mprog and mprog/let are mutually recursive, we:

  1. Declare and give modes for both type families before declaring their constants.
  2. Declare their worlds simulataneously, by putting two call-patterns in the world declaration.
  3. Prove them total simultaneously, with the mutual termination order (M E).

And thus we have proved type safety for MinML with monadic effects!

Summer school 2008
Previous: Exercies 3