POPL Tutorial/Exceptions-problem

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

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

Types:

tp : type.				%name tp T.
nat : tp.
arr : tp -> tp -> tp.

Raw expressions, which admit ill-typed terms

exp : type.				%name exp E.
z : exp.
s : exp -> exp.
ifz : exp -> exp -> (exp -> exp) -> exp.
fun : tp -> tp -> (exp -> exp -> exp) -> exp.
app : 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.

raise : tp -> exp.
handle : exp -> exp -> exp.

Static semantics

A judgement picking out the well-typed terms:

of : exp -> tp -> type.			%name of Dof.
%mode of +E -T.

of/z
   : of z nat.
of/s
   : of (s E) nat <- of E nat.
of/ifz
   : of (ifz E E1 ([x] E2 x)) T
      <- of E nat
      <- of E1 T
      <- ({x:exp} of x nat -> of (E2 x) T).
of/fun
   : of (fun T1 T2 ([f] [x] E f x)) (arr T1 T2)
      <- ({f:exp} of f (arr T1 T2) -> {x:exp} of x T1 -> of (E f x) T2).
of/app
   : 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).

of/raise
   : of (raise T) T.
of/handle
   : of (handle E1 E2) T
      <- of E1 T
      <- of E2 T.

Dynamic semantics

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

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

raises : exp -> type.
%mode raises +E.

raises/raise   
   : raises (raise T).
raises/app/fun
   : raises (app E1 E2)
      <- raises E1.
raises/app/arg
   : 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.

step : exp -> 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.

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.

step/handle/body
   : step
      (handle E1 E2)
      (handle E1' E2)
      <- step E1 E1'.
step/handle/raise
   : step
      (handle E1 E2)
      E2
      <- raises E1. 
step/handle/body-v
   : 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.

pres : step E E' -> of E T -> of E' T -> type. %name pres Dpres.
%mode pres +Dstep +Dof -Dof.

- : pres
     (step/s Dstep)
     (of/s Dof)
     (of/s Dof')
     <- pres Dstep Dof Dof'.

- : 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'.

- : pres
     step/ifz/z
     (of/ifz _ Dof1 _)
     Dof1.

- : pres
     (step/ifz/s (_ : value E))
     (of/ifz ([x] [dx] Dof2 x dx) _ (of/s Dof))
     (Dof2 E Dof).

- : pres
     (step/app/fun Dstep1)
     (of/app Dof2 Dof1)
     (of/app Dof2 Dof1')
     <- pres Dstep1 Dof1 Dof1'.

- : pres
     (step/app/arg Dstep2 _)
     (of/app Dof2 Dof1)
     (of/app Dof2' Dof1)
     <- pres Dstep2 Dof2 Dof2'.

- : 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

val-or-raises-or-step : exp -> type.		%name val-or-raises-or-step Dvrs.
vrs/val : val-or-raises-or-step E <- value E.
vrs/step : val-or-raises-or-step E <- step E _.

val-or-raises-or-step must have a case for when an expression raises an exception.

vrs/raises : val-or-raises-or-step E <- raises E.

Factoring lemmas

prog/s
   : val-or-raises-or-step E -> val-or-raises-or-step (s E) -> type.
%mode prog/s +Dvrs1 -Dvrs2.

- : prog/s
     (vrs/step Dstep)
     (vrs/step (step/s Dstep)).

- : prog/s
     (vrs/val Dval)
     (vrs/val (value/s Dval)).

A new case for when the input is an unhandled exception must be provided.

- : prog/s
     (vrs/raises Draises)
     (vrs/raises (raises/s Draises)).

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

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

- : prog/ifz _ (vrs/step Dstep) _ _ (vrs/step (step/ifz/arg Dstep)).
- : prog/ifz _ (vrs/val value/z) _ _ (vrs/step step/ifz/z).
- : 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.

- : prog/ifz _ (vrs/raises Draises) _ _ (vrs/raises (raises/ifz Draises)).
%worlds () (prog/ifz _ _ _ _ _).
%total {} (prog/ifz _ _ _ _ _).

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)
      -> type.
%mode prog/app +Dof +Dvrs1 +Dvrs2 -Dstep.

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

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

- : 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

prog : of E T -> val-or-raises-or-step E -> type. %name prog Dprog.
%mode prog +Dof -Dvrs.

- : prog of/z (vrs/val value/z).

- : prog (of/s Dof) Dvrs'
     <- prog Dof Dvrs
     <- prog/s Dvrs Dvrs'.

- : prog (of/ifz ([x] [dx] Dof2 x dx) Dof1 Dof) Dvrs'
     <- prog Dof Dvrs
     <- prog/ifz Dof Dvrs _ _ Dvrs'.

- : prog (of/fun _) (vrs/val value/fun).

- : 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 _).