POPL Tutorial/Exceptions-problem
Type safety for MinML: call-by-value, with recursive functions, in extrinsic form, with exceptions.
In this example, we will take the MinML language from earlier and extend it with constructs for raising and handling exceptions.
The static semantics will be extended with rules to handle these new expressions. The structured operational semantics from before will be extended with a new judgment that denotes when an expression raises an uncaught exception.
The preservation and progress proofs must then be updated to accommodate the extensions to the language.
Syntax
Section titled “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 %.We will extend MinML with two constructs. The first, (raise T), is a term of type T that will raise an exception.
The second, (handle E1 E2), is a term that executes E1. If E1 evaluates to a value V, then (handle E1 E2) evaluates to V. If E1 raises an exception, then the handler E2 is executed.
%term raise %pi tp %-> exp %.%term handle %pi exp %-> exp %-> exp %.Static semantics
Section titled “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) %.The following are the new typing rules for (raise T) and (handle E1 E2).
%term of/raise of (raise T) T %.%term of/handle %pi (of (handle E1 E2) T) %<- (of E1 T) %<- (of E2 T) %.Dynamic semantics
Section titled “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) %.Exercise: Give two rules, raises/s and raises/ifz, that propogate raises through the (s E) and (ifz E1 E2 E3) expressions.
%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) %.The following are new step rules for the (handle E1 E2) expression. There is one rule for stepping the body, another rule for handling a raised exception, and a third rule for when the body is a value.
%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
Section titled “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) %.Exercise: Give proof cases for step/handle/body, step/handle/body-v, and step/handle/raise.
%worlds () (pres Dstep Dof Dof') %.%total Dstep (pres Dstep _ _) %.Progress
Section titled “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 _) %.val-or-raises-or-step must have a case for when an expression raises an exception.
%term vrs/raises %pi (val-or-raises-or-step E) %<- (raises E) %.%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)) %.A new case for when the input is an unhandled exception must be provided.
%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)) %.A new case for when the input is an unhandled exception must be provided.
%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)) %.Exercise: Give the missing cases for when the inputs are unhandled exceptions.
%worlds () (prog/app _ _ _ _) %.%total {} (prog/app _ _ _ _) %.Main theorem
Section titled “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) %.Exercise: Give the missing cases for of/handle and of/raise. It may be necessary to use a factoring lemma in the solution for the case corresponding to of/handle.
%worlds () (prog _ _) %.%total Dof (prog Dof _) %.