CIS 500Software FoundationsFall 2006October 25A Little More on ReferencesRecapLast time, we discussed how to formalize languages with mutablestate...SyntaxWe added to λ→(with Unit) syntactic forms for creating,dereferencing, and assigning reference cells, plus a new typeconstructor Ref.t ::= termsunit unit constantx variableλx:T.t abstractiont t applicationref t reference creation!t dereferencet:=t assignmentl store locationEvaluationEvaluation becomes a four-place relation: t | µ −→ t0| µ0l /∈ dom(µ)ref v1| µ −→ l | (µ, l 7→ v1)(E-RefV)µ(l) = v!l | µ −→ v | µ(E-DerefLoc)l:=v2| µ −→ unit | [l 7→ v2]µ(E-Assign)(Plus several congruence rules.)TypingTyping becomes a three-place relation: Γ | Σ ` t : TΣ(l) = T1Γ | Σ ` l : Ref T1(T-Loc)Γ | Σ ` t1: T1Γ | Σ ` ref t1: Ref T1(T-Ref)Γ | Σ ` t1: Ref T11Γ | Σ ` !t1: T11(T-Deref)Γ | Σ ` t1: Ref T11Γ | Σ ` t2: T11Γ | Σ ` t1:=t2: Unit(T-Assign)PreservationTheorem: IfΓ | Σ ` t : TΓ | Σ ` µt | µ −→ t0| µ0then, for some Σ0⊇ Σ,Γ | Σ0` t0: TΓ | Σ0` µ0.ProgressTheorem: Suppose t is a closed, well-typed term (that is,∅ | Σ ` t : T for some T and Σ). Then either t is a value or else,for any store µ such that ∅ | Σ ` µ, there is some term t0and storeµ0with t | µ −→ t0| µ0.Nontermination via referencesThere are well-typed terms in this system that are not stronglynormalizing. For example:t1 = λr:Ref (Unit→Unit).(r := (λx:Unit. (!r)x);(!r) unit);t2 = ref (λx:Unit. x);Applyingt1 to t2 yields a (well-typed) divergent term.Recursion via referencesIndeed, we can define arbitrary recursive functions using references.1. Allocate a ref cell and initialize it with a dummy function ofthe appropriate type:factref= ref (λn:Nat.0)2. Define the body of the function we are interested in, using thecontents of the reference cell for making recursive calls:factbody=λn:Nat.if iszero n then 1 else times n ((!factref)(pred n))3. “Backpatch” by storing the real body into the reference cell:factref:= factbody4. Extract the contents of the reference cell and use it as desired:fact = !factreffact 5ExceptionsMotivationMost programming languages provide some mechanism forinterrupting the normal flow of control in a program to signal someexceptional condition.Note that it is always possible to program without exceptions —instead of raising an exc eption, we return None; instead ofreturning res ult x normally, we return Some(x). But now we needto wrap every function application in a case to fi nd out whether itreturned a result or an exception.It is much more convenient to build this mechanism into thelanguage.Varieties of non-local controlThere are many ways of adding “non-local control flow”Iexit(1)IgotoIsetjmp/longjmpIraise/try (or catch/throw) in many variationsIcallcc / continuationsImore esoteric variants (cf. many Scheme papers)Let’s b e gin with the s implest of these.An “abort” primitive in λ→First step: raising exceptions (but not catching them).t ::= ... termserror run-time errorEvaluationerror t2−→ error(E-AppErr1)v1error −→ error(E-AppErr2)IWhat if we had booleans and numbers in the language?TypingTypingΓ ` error : T(T-Error)Typing errorsNote that the typing rule for error allows us to give it any type T.Γ ` error : T(T-Error)This means that b othif x>0 then 5 else errorandif x>0 then true else errorwill typecheck.Aside: Syntax-directednessNote that this ruleΓ ` error : T(T-Error)has a problem from the point of view of implementation: it is notsyntax directed.This will cause the Uniqueness of Types theorem to fail.For purposes of defining the language and proving its type safety,this is not a problem — Uniqueness of Types is not critical.Let’s think a little, though, about how t he rule might be fixed...An alternativeCan’t we just decorate the error keyword with its intended type,as we have done to fix related problems with other constructs?Γ ` (error as T) : T(T-Error)No, this do e sn’t work!E.g. (assuming our language also has numbers and booleans):succ (if (error as Bool) then 5 else 7)−→ succ (error as Bool)Exercise: Come up with a similar example using just functions anderror.An alternativeCan’t we just decorate the error keyword with its intended type,as we have done to fix related problems with other constructs?Γ ` (error as T) : T(T-Error)No, this do e sn’t work!E.g. (assuming our language also has numbers and booleans):succ (if (error as Bool) then 5 else 7)−→ succ (error as Bool)Exercise: Come up with a similar example using just functions anderror.Another alternativeIn a system with universal polymorphism (like OCaml), thevariability of typing for error can be dealt with by assigning it avariable type!Γ ` error :0a(T-Error)In effect, we are replacing the uniqueness of typing property by aweaker (but still very useful) property called most general typing.I.e., although a term may have many types, we always have acompact way of representing the set of all of its possible types.Yet another alternativeAlternatively, in a system with subtyping (which we’ll discuss in thenext lecture) and a minimal Bot type, we can give error a uniquetype:Γ ` error : Bot(T-Error)(Of course, what we’ve really done is just pushed the complexity ofthe old error rule onto the Bot type! We’ll return to this pointlater.)For now...Let’s stick with the original ruleΓ ` error : T(T-Error)and live with the resulting nondeterminism of the typing relation.Type safetyThe preservation theorem requires no changes when we add error:if a term of type T reduces to error, that’s fine, since error hasevery type T.Progress, though, requires a litte more care.Type safetyThe preservation theorem requires no changes when we add error:if a term of type T reduces to error, that’s fine, since error hasevery type T.Progress, though, requires a litte more care.ProgressFirst, note that we do not want to extend the set of values toinclude error, since this would make our new rule for propagatingerrors through applications.v1error −→ error(E-AppErr2)overlap with our existing computation rule for applications:(λx:T11.t12) v2−→ [x 7→ v2]t12(E-AppAbs)e.g., the term(λx:Nat.0) errorcould evaluate to either 0 (which would be wrong) or error(which is what we intend).ProgressInstead, we keep error as a non-value normal form, and refine thestatement of progress to explicitly mention the possibility thatterms may evaluate to error instead of to a
View Full Document