Summer school 2008:Type safety for MinML with monadic effects

Type safety for MinML with monadic effects

Syntax / static semantics

Types:

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.
%term circle %pi 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.

%sort exp {_ tp} %.
%name exp %.
%prec %postfix 1 exp %.
%sort command {_ tp} %.
%name command %.
%prec %postfix 1 command %.
%term z nat exp %.
%term s %pi (nat exp) %-> (nat exp) %.
%term ifz %pi (nat exp) %-> (T exp) %-> (%pi (nat exp) %-> (T exp)) %-> (T exp) %.
%term fun {T1 tp} {T2 tp} %pi (%pi (arr T1 T2 exp) %-> (T1 exp) %-> (T2 exp)) %-> (arr T1 T2 exp) %.
%term app %pi (arr T1 T2 exp) %-> (T1 exp) %-> (T2 exp) %.
%term comp %pi (T command) %-> (circle T exp) %.
%term return %pi (T exp) %-> (T command) %.
%term let %pi (circle T exp) %-> (%pi (T exp) %-> (U command)) %-> (U command) %.

Dynamic semantics / preservation

Values and final states

%sort value {_ T exp} %.
%name value %.
%mode value %in %.
%term value/z value z %.
%term value/s %pi (value (s E)) %<- (value E) %.
%term value/fun value (fun _ _ _) %.
%term value/comp value (comp _) %.
%sort final {_ T command} %.
%name final %.
%mode final %in %.
%term final/ret %pi (final (return E)) %<- (value E) %.

Transition relation for expressions

%sort step {_ T exp} {_ T exp} %.
%name step %.
%mode step %in %out %.
%term step/s %pi (step (s E) (s E')) %<- (step E E') %.
%term step/ifz/arg %pi (step (ifz E E1 ([x] E2 x)) (ifz E' E1 ([x] E2 x))) %<- (step E E') %.
%term step/ifz/z step (ifz z E1 ([x] E2 x)) E1 %.
%term step/ifz/s %pi (step (ifz (s E) E1 ([x] E2 x)) (E2 E)) %<- (value E) %.
%term step/app/fun %pi (step (app E1 E2) (app E1' E2)) %<- (step E1 E1') %.
%term step/app/arg %pi (step (app E1 E2) (app E1 E2')) %<- (value E1) %<- (step E2 E2') %.
%term step/app/beta-v
  %pi (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

%sort mstep {_ T command} {_ T command} %.
%name mstep %.
%mode mstep %in %out %.
%term mstep/ret %pi (mstep (return E) (return E')) %<- (step E E') %.
%term mstep/let-e %pi (mstep (let E ([x] M x)) (let E' ([x] M x))) %<- (step E E') %.
%term mstep/let-m
  %pi (mstep (let (comp M1) ([x] M2 x)) (let (comp M1') ([x] M2 x)))
  %<- (mstep M1 M1') %.
%term mstep/let-beta %pi (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

%sort val-or-step {_ T exp} %.
%name val-or-step %.
%term vos/val %pi (val-or-step E) %<- (value E) %.
%term vos/step %pi (val-or-step E) %<- (step E _) %.
%sort fin-or-mstep {_ T command} %.
%name fin-or-mstep %.
%term fos/fin %pi (fin-or-mstep M) %<- (final M) %.
%term fos/step %pi (fin-or-mstep M) %<- (mstep M _) %.

Factoring lemmas

%sort prog/s {_ val-or-step E} {_ val-or-step (s E)} %.
%mode prog/s %in %out %.
%term _ prog/s (vos/step Dstep) (vos/step (step/s Dstep)) %.
%term _ prog/s (vos/val Dval) (vos/val (value/s Dval)) %.
%worlds () (prog/s _ _) %.
%total {} (prog/s _ _) %.
%sort prog/ifz {_ val-or-step (%the (nat exp) E)} {E1} {E2} {_ step (ifz E E1 ([x] E2 x)) E'} %.
%mode prog/ifz %in %in %in %out %.
%term _ prog/ifz (vos/step Dstep) _ _ (step/ifz/arg Dstep) %.
%term _ prog/ifz (vos/val value/z) _ _ step/ifz/z %.
%term _ prog/ifz (vos/val (value/s Dval)) _ _ (step/ifz/s Dval) %.
%worlds () (prog/ifz _ _ _ _) %.
%total {} (prog/ifz _ _ _ _) %.
%sort prog/app {_ val-or-step (%the (arr T2 T exp) E1)} {_ val-or-step (%the (T2 exp) E2)} {_ step (app E1 E2) E'} %.
%mode prog/app %in %in %out %.
%term _ prog/app (vos/step Dstep1) _ (step/app/fun Dstep1) %.
%term _ prog/app (vos/val Dval1) (vos/step Dstep2) (step/app/arg Dstep2 Dval1) %.
%term _ prog/app (vos/val Dval1) (vos/val Dval2) (step/app/beta-v Dval2) %.
%worlds () (prog/app _ _ _) %.
%total {} (prog/app _ _ _) %.

Progress for expressions

%sort prog {E T exp} {_ val-or-step E} %.
%name prog %.
%mode prog %in %out %.
%term _ prog z (vos/val value/z) %.
%term _ %pi (prog (s E) Dvos') %<- (prog E Dvos) %<- (prog/s Dvos Dvos') %.
%term _
  %pi (prog (ifz E E1 ([x] E2 x)) (vos/step Dstep))
  %<- (prog E Dvos)
  %<- (prog/ifz Dvos _ _ Dstep) %.
%term _ prog (fun _ _ _) (vos/val value/fun) %.
%term _
  %pi (prog (app E1 E2) (vos/step Dstep))
  %<- (prog E1 Dvos1)
  %<- (prog E2 Dvos2)
  %<- (prog/app Dvos1 Dvos2 Dstep) %.
%term _ prog (comp M) (vos/val value/comp) %.
%worlds () (prog _ _) %.
%total Dof (prog Dof _) %.

Factoring lemmas for commands

%sort mprog/ret {_ val-or-step E} {_ fin-or-mstep (return E)} %.
%mode mprog/ret %in %out %.
%term _ mprog/ret (vos/val Dval) (fos/fin (final/ret Dval)) %.
%term _ mprog/ret (vos/step Dstep) (fos/step (mstep/ret Dstep)) %.
%worlds () (mprog/ret _ _) %.
%total {} (mprog/ret _ _) %.
%sort mprog/let-comp {_ fin-or-mstep (%the (T command) M1)} {M2 %pi (T exp) %-> (U command)} {_ mstep (let (comp M1) M2) M'} %.
%mode mprog/let-comp %in %in %out %.
%term _ mprog/let-comp (fos/fin (%the (final (return E)) (final/ret Dval))) M2 (%the (mstep (let (comp (return E)) M2) (M2 E)) (mstep/let-beta (final/ret Dval))) %.
%term _ mprog/let-comp (fos/step (%the (mstep M1 M1') Dmstep)) M2 (%the (mstep (let (comp M1) M2) (let (comp M1') M2)) (mstep/let-m Dmstep)) %.
%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.

%sort mprog/let {E circle T exp} {_ val-or-step E} {M %pi (T exp) %-> (U command)} {_ mstep (let E M) M'} %.
%mode mprog/let %in %in %in %out %.
%sort mprog {M T command} {_ fin-or-mstep M} %.
%mode mprog %in %out %.
%% mprog/let
%term _
  %pi (mprog/let (comp M) (vos/val value/comp) _ Dmstep)
  %<- (mprog M Dfos)
  %<- (mprog/let-comp Dfos _ Dmstep) %.
%term _ mprog/let _ (vos/step Dstep) _ (mstep/let-e Dstep) %.
%% mprog
%term _ %pi (mprog (return E) Dfos) %<- (prog E Dvos) %<- (mprog/ret Dvos Dfos) %.
%term _
  %pi (mprog (let (%the (circle T exp) E) (%the (%pi (T exp) %-> (U command)) M)) (fos/step Dmstep))
  %<- (prog E (%the (val-or-step E) Dvos))
  %<- (mprog/let E Dvos M (%the (mstep (let E M) M') Dmstep)) %.
%worlds () (mprog _ _) (mprog/let _ _ _ _) %.
%total (M E) (mprog M _) (mprog/let E _ _ _) %.

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

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

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