POPL Tutorial/Exceptions

Type safety for MinML: call-by-value, with recursive functions, in extrinsic form, with exceptions

Syntax

Types:

%sort tp %.
%name tp %.
%term nat tp %.
%term arr %pi tp %-> tp %-> tp %.

Raw expressions, which admit ill-typed terms

%sort exp %.
%name exp %.
%term z exp %.
%term s %pi exp %-> exp %.
%term ifz %pi exp %-> exp %-> (%pi exp %-> exp) %-> exp %.
%term fun %pi tp %-> tp %-> (%pi exp %-> exp %-> exp) %-> exp %.
%term app %pi exp %-> exp %-> exp %.
%term raise %pi tp %-> exp %.
%term handle %pi exp %-> exp %-> exp %.

Static semantics

A judgement picking out the well-typed terms:

%sort of {_ exp} {_ tp} %.
%name of %.
%mode of %in %out %.
%term of/z of z nat %.
%term of/s %pi (of (s E) nat) %<- (of E nat) %.
%term of/ifz
  %pi (of (ifz E E1 ([x] E2 x)) T)
  %<- (of E nat)
  %<- (of E1 T)
  %<- ({x exp} %pi (of x nat) %-> (of (E2 x) T)) %.
%term of/fun
  %pi (of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2))
  %<- ({f exp} %pi (of f (arr T1 T2)) %-> ({x exp} %pi (of x T1) %-> (of (E f x) T2))) %.
%term of/app %pi (of (app E1 E2) T) %<- (of E1 (arr T2 T)) %<- (of E2 T2) %.
%term of/raise of (raise T) T %.
%term of/handle %pi (of (handle E1 E2) T) %<- (of E1 T) %<- (of E2 T) %.

Dynamic semantics

%sort value {_ 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 _ _ _) %.
%sort raises {_ exp} %.
%mode raises %in %.
%term raises/raise raises (raise T) %.
%term raises/app/fun %pi (raises (app E1 E2)) %<- (raises E1) %.
%term raises/app/arg %pi (raises (app E1 E2)) %<- (value E1) %<- (raises E2) %.
%term raises/s %pi (raises (s E)) %<- (raises E) %.
%term raises/ifz %pi (raises (ifz E1 E2 E3)) %<- (raises E1) %.
%sort step {_ exp} {_ 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) %.
%term step/handle/body %pi (step (handle E1 E2) (handle E1' E2)) %<- (step E1 E1') %.
%term step/handle/raise %pi (step (handle E1 E2) E2) %<- (raises E1) %.
%term step/handle/body-v %pi (step (handle E1 E2) E1) %<- (value E1) %.

Preservation

With this encoding, we have to prove preservation explicitly, as the type of step doesn’t guarantee it.

%sort pres {_ step E E'} {_ of E T} {_ of E' T} %.
%name pres %.
%mode pres %in %in %out %.
%term _ %pi (pres (step/s Dstep) (of/s Dof) (of/s Dof')) %<- (pres Dstep Dof Dof') %.
%term _
  %pi (pres (step/ifz/arg Dstep) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof'))
  %<- (pres Dstep Dof Dof') %.
%term _ pres step/ifz/z (of/ifz _ Dof1 _) Dof1 %.
%term _ pres (step/ifz/s (%the (value E) _)) (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof)) (Dof2 E Dof) %.
%term _
  %pi (pres (step/app/fun Dstep1) (of/app Dof2 Dof1) (of/app Dof2 Dof1'))
  %<- (pres Dstep1 Dof1 Dof1') %.
%term _
  %pi (pres (step/app/arg Dstep2 _) (of/app Dof2 Dof1) (of/app Dof2' Dof1))
  %<- (pres Dstep2 Dof2 Dof2') %.
%term _ pres (step/app/beta-v _) (of/app Dof2 (of/fun ([f] [df] [x] [dx] Dof1 f df x dx))) (Dof1 _ (of/fun ([f] [df] [x] [dx] Dof1 f df x dx)) _ Dof2) %.
%term _
  %pi (pres (step/handle/body Dstep) (of/handle Dof2 Dof1) (of/handle Dof2 Dof1'))
  %<- (pres Dstep Dof1 Dof1') %.
%term _ pres (step/handle/raise Draise) (of/handle Dof2 Dof1) Dof2 %.
%term _ pres (step/handle/body-v Dval) (of/handle Dof2 Dof1) Dof1 %.
%worlds () (pres Dstep Dof Dof') %.
%total Dstep (pres Dstep _ _) %.

Progress

%sort val-or-raises-or-step {_ exp} %.
%name val-or-raises-or-step %.
%term vrs/val %pi (val-or-raises-or-step E) %<- (value E) %.
%term vrs/step %pi (val-or-raises-or-step E) %<- (step E _) %.
%term vrs/raises %pi (val-or-raises-or-step E) %<- (raises E) %.

Factoring lemmas

%sort prog/s {_ val-or-raises-or-step E} {_ val-or-raises-or-step (s E)} %.
%mode prog/s %in %out %.
%term _ prog/s (vrs/step Dstep) (vrs/step (step/s Dstep)) %.
%term _ prog/s (vrs/val Dval) (vrs/val (value/s Dval)) %.
%term _ prog/s (vrs/raises Draises) (vrs/raises (raises/s Draises)) %.
%worlds () (prog/s _ _) %.
%total {} (prog/s _ _) %.
%sort prog/ifz {_ of E nat} {_ val-or-raises-or-step E} {E1} {E2} {_ val-or-raises-or-step (ifz E E1 ([x] E2 x))} %.
%mode prog/ifz %in %in %in %in %out %.
%term _ prog/ifz _ (vrs/step Dstep) _ _ (vrs/step (step/ifz/arg Dstep)) %.
%term _ prog/ifz _ (vrs/val value/z) _ _ (vrs/step step/ifz/z) %.
%term _ prog/ifz _ (vrs/val (value/s Dval)) _ _ (vrs/step (step/ifz/s Dval)) %.
%term _ prog/ifz _ (vrs/raises Draises) _ _ (vrs/raises (raises/ifz Draises)) %.
%worlds () (prog/ifz _ _ _ _ _) %.
%total {} (prog/ifz _ _ _ _ _) %.
%sort prog/app {_ of E1 (arr T2 T)} {_ val-or-raises-or-step E1} {_ val-or-raises-or-step E2} {_ val-or-raises-or-step (app E1 E2)} %.
%mode prog/app %in %in %in %out %.
%term _ prog/app _ (vrs/step Dstep1) _ (vrs/step (step/app/fun Dstep1)) %.
%term _ prog/app _ (vrs/val Dval1) (vrs/step Dstep2) (vrs/step (step/app/arg Dstep2 Dval1)) %.
%term _ prog/app _ (vrs/val Dval1) (vrs/val Dval2) (vrs/step (step/app/beta-v Dval2)) %.
%term _ prog/app _ (vrs/raises Draise1) _ (vrs/raises (raises/app/fun Draise1)) %.
%term _ prog/app _ (vrs/val Dval1) (vrs/raises Draise2) (vrs/raises (raises/app/arg Draise2 Dval1)) %.
%worlds () (prog/app _ _ _ _) %.
%total {} (prog/app _ _ _ _) %.
%sort prog/handle {_ val-or-raises-or-step E1} {E2} {_ val-or-raises-or-step (handle E1 E2)} %.
%mode prog/handle %in %in %out %.
%term _ prog/handle (vrs/val Dval) _ (vrs/step (step/handle/body-v Dval)) %.
%term _ prog/handle (vrs/raises Draise) _ (vrs/step (step/handle/raise Draise)) %.
%term _ prog/handle (vrs/step Dstep) _ (vrs/step (step/handle/body Dstep)) %.
%worlds () (prog/handle _ _ _) %.
%total {} (prog/handle _ _ _) %.

Main theorem

%sort prog {_ of E T} {_ val-or-raises-or-step E} %.
%name prog %.
%mode prog %in %out %.
%term _ prog of/z (vrs/val value/z) %.
%term _ %pi (prog (of/s Dof) Dvrs') %<- (prog Dof Dvrs) %<- (prog/s Dvrs Dvrs') %.
%term _
  %pi (prog (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) Dvrs')
  %<- (prog Dof Dvrs)
  %<- (prog/ifz Dof Dvrs _ _ Dvrs') %.
%term _ prog (of/fun _) (vrs/val value/fun) %.
%term _
  %pi (prog (of/app Dof2 Dof1) Dvrs3)
  %<- (prog Dof1 Dvrs1)
  %<- (prog Dof2 Dvrs2)
  %<- (prog/app Dof1 Dvrs1 Dvrs2 Dvrs3) %.
%term _
  %pi (prog (of/handle Dof2 Dof1) Dvrs2)
  %<- (prog Dof1 Dvrs1)
  %<- (prog/handle Dvrs1 _ Dvrs2) %.
%term _ prog of/raise (vrs/raises raises/raise) %.
%worlds () (prog _ _) %.
%total Dof (prog Dof _) %.

And thus we have proved type safety for minml with exceptions!