DOC PREVIEW
Penn CIS 500 - CIS 500 LECTURE NOTES

This preview shows page 1-2 out of 6 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 6 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

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

Penn CIS 500 - CIS 500 LECTURE NOTES

Download CIS 500 LECTURE NOTES
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view CIS 500 LECTURE NOTES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CIS 500 LECTURE NOTES 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?