***************************** 505 Final Exam ******************************** Instructions: Due Friday Dec. 8 at 4:30pm. Open notes, but no collaboration nor searching for answers on the web etc. You may do anything you like before looking at the exam, but only look at previously gathered materials after looking at the exam. Take in a single, 4-hour period, self-timed. You may develop your solutions on-line, including testing out your solutions using the Scheme and SML interpreters. For short-answer questions, you shouldn't need to write more than 100-200 words or so, and for most questions a few dozen words in telegraphese should be sufficient. You should edit this file to include your answers (do not use an editor that doesn't wrap your text at 80 columns) and email your solution to {todd,lerns,chambers}@cs. 100 points total. ----------------------------------------------------------------------------- Name: ----------------------------------------------------------------------------- 1) Translate the following ML declarations into Core ML declarations (for ML datatypes, only do the types, not any associated constructor functions or values), or explain what is wrong with the ML declarations, or explain why the legal ML declaration can't be expressed in Core ML. a) [3 pts] datatype ('a, 'b) Table = table of ('a*'b) list type Table = forall a. forall b. branded Table {table: list[a*b]}. b) [3 pts] val f: ('a -> 'b) * 'b -> ('c -> 'b) -> 'c = ... val f: forall a. forall b. forall c. (a->b) * b -> (c->b) -> c = ... ---------------------------------------------------------------------------- 2) Translate the following Core ML declarations into ML declarations, or explain what is wrong with the Core ML declarations, or explain why the legal Core ML declaration can't be expressed in ML. a) [3 pts] type F = rec t = [Some:{x:t, y:F, z:t}, None:int] Illegal Core ML declaration: F isn't defined. b) [3 pts] type G = rec t = {a:int, b:t} datatype G = g of {a:int, b:G} (But we can't make values of this type, since there's no base case.) c) [3 pts] type H = [Frob:int, Fribble:string, Qux:bool->bool] datatype H = Frob of int | Fribble of string | Qux of bool->bool d) [3 pts] type F = forall a. (a -> (forall b. (a*b -> b))) Can't be translated, since ML doesn't support nested foralls, only outermost foralls (a property of let polymorphism). ----------------------------------------------------------------------------- 3) For each of the following unifications, written tau1 == tau2, give the resulting unified type, or explain why there is no unification. In the examples, unconstrained type variables are written like 'a. a) [3 pts] 'a * ('b -> 'c) == ('c -> 'd) * (('c * 'd) -> int) a = c->d b = c*d c = int (int -> 'd) * ((int * 'd) -> int) b) [3 pts] 'a * ('b -> 'c) == ('d * 'e) -> 'f Doesn't unify, since * and -> don't match c) [3 pts] ('a -> 'b) * 'b == (int -> ('c * string)) * (bool * 'd) a = int b = 'c * string b = bool * 'd (int -> (bool * string)) * (bool * string) d) [3 pts] 'a * 'c == ('b -> 'c) * 'a a = b->c c = a Doesn't unify, since it would create a cycle: ('b -> ('b -> ('b -> ...))) * ('b -> ('b -> ('b -> ...))) e) [2 pts] If during type inference, two types don't unify, what does it mean? A type checking error ---------------------------------------------------------------------------- 4) [3 pts] What is the difference between forall and Lambda? Give an example illustrating the difference. forall allows a polymorphic *type* to be described, while Lambda allows a *value* of a polymorphic type to be constructed. E.g.: type list = forall T. ... is the *type* of lists, which is polymorphic in the type of the elements, while val nil:list = Lambda T. ... is the *value* of empty lists, which is polymorphic in the type of the elements of the lists it is the end of. When a polymorphic type is instantiated, a type results, while when a polymorphic value is instantiated, a value results. ---------------------------------------------------------------------------- 5) For each of the following examples, indicate whether or not the two types are in the indicated subtyping relation, and if not, explain why not. Assume that int <= num, float <= num, num <= Object, bool <= Object, and string <= Object. a) [3 pts] {x:int, y:bool, z:string} <= {y:bool, x:int} True b) [3 pts] [a:int, b:bool] <= [a:num, b:Object, c:int] True c) [3 pts] (int->Object) -> (num->string) <= (num->string) -> (int->Object) True d) [3 pts] ({x:int, y:int, z:int} -> [i:int]) <= ({x:int, y:int} -> [i:int, j:int]) False: the argument types are not in the contravariant relation. ---------------------------------------------------------------------------- 6) Translate the following class declarations into Core ML (with references and subtyping) types and values, as in lecture notes #18.4. a) [4 pts] class Foo { var x:int; (* an immutable instance variable *) method baz(arg:Foo):Foo { if arg.x > self.x then return arg else return self; } } val foo:Foo = new Foo(3); type Foo = rec Foo = {x:int, baz:Foo->Foo} val foo:Foo = rec self:Foo = {x=3, baz=(lambda(arg:Foo). if arg.x > self.x then arg else self)} b) [4 pts] class Baz[T] extends Foo { var y:T; method biz():T { return self.y; } } val baz:Baz[string] = new Baz[string](4, "hi"); type Baz = forall T. rec Baz = {x:int, y:T, baz:Foo->Foo, biz:unit->T} val baz:Baz[string] = rec self:Baz[string] = {x=4, y="hi", baz=(lambda(arg:Foo). if arg.x > self.x then arg else self), biz=(lambda(). self.y)} c) [4 pts] class Qux extends Baz[bool] { method baz(arg:Foo):Foo { return self; } } val qux:Qux = new Qux(5, true); type Qux = rec Qux = {x:int, y:bool, baz:Foo->Foo, biz:unit->bool} val qux:Qux = rec self:Qux = {x=5, y=true, baz=(lambda(arg:Foo). self), biz=(lambda(). self.y)} d) [2 pts] Explain what kinds of changes to the argument and result types of the baz method in the Qux class would still be type-correct. The argument type can be any supertype of Foo, and the result type can be any subtype of Foo. e) [3 pts] Is Baz[bool] a subtype of Baz[Object]? Explain why or why not. Yes, because the type parameter T only appears in covariant/positive positions in the type Baz, and bool <= Object. ---------------------------------------------------------------------------- 7) [4 pts] The object encodings we saw only supported immutable instance variables. How would you encode mutable instance variables (in Core ML without the mutable record extension)? Demonstrate your encoding on the following example: class P { var x:int; (* a *mutable* instance variable *) var y:int; method p():unit { x := y; } } val p:P = new P(3,4); (* new P(3,4) just builds an instance of P whose x & y instance variables are initialized to 3 and 4, respectively *) I would use refs for the instance variables. type P = {x:ref[int], y:ref[int], p:unit->unit} val p:P = rec self:P = {x=ref[int] 3, y=ref[int] 4, p=(lambda(). self.x := !self.x)} ----------------------------------------------------------------------------- 8) Components of records are immutable in Core ML. We might like to add direct support for mutable record components in Core ML. The new language constructs are the following: tau ::= ... | {var id1:tau1, ..., var idN:tauN} e ::= ... | {var id1=e1, ..., var idN=eN} | #idi e | #idi e1 := e2 | e1; e2 These new mutable record constructs are in addition to the existing immutable record constructs. A mutable record type like "{var x:int, var y:bool}" is the type of record values whose components can be updated in place. A mutable record constructor expression like "{var x = 3, var y = true}" creates a new mutable record value. Both the existing immutable records and the new mutable records can be accessed using a record projection expression like "#x e", but mutable records can be updated in place using record update expressions like "#x e := 5" (record updates return (), the value of type unit). [Assume that there is a base type "unit" already in tau, and a base constant "()" already in e.] To make side-effecting operations easier to write, we add the sequence expression form "e1; e2", whose semantics is to evaluate e1, then throw its result away, then evaluate e2, whose result becomes the result of the sequence expression. (For simplicity, we will ignore pattern-matching in this question.) Your task is to formalize the semantics of these new constructs. a) [7 pts] Give typing rules for these new constructs, in the style of judgments from lecture notes #9. Give the *full* typing rules for all uses of record projection. Also explain informally what your rules are trying to accomplish. Check mutable record constructors: Gamma |- e1 : tau1 ... Gamma |- eN : tauN -------------------- Gamma |- {var id1=e1, ..., var idN=eN} : {var id1:tau1, ..., var idN:tauN} Record projection works on both immutable and mutable records: Gamma |- e : {id1:tau1, ..., idN:tauN} 1 <= i <= N -------------------- Gamma |- (#idi e) : taui Gamma |- e : {var id1:tau1, ..., var idN:tauN} 1 <= i <= N -------------------- Gamma |- (#idi e) : taui Record assignment works on mutable records, and verifies that the component being updated has the same type as the rhs expression: Gamma |- e1 : {id1:tau1, ..., idN:tauN} 1 <= i <= N Gamma |- e2 : taui -------------------- Gamma |- (#idi e1 := e2) : unit Sequencing ignores the type of the first expression (but it does have to check that it has some type!): Gamma |- e1 : tau1 Gamma |- e2 : tau2 -------------------- Gamma |- (e1; e2) : tau2 b) [7 pts] Give a big-step operational semantics for these constructs, in the style of lecture notes #14. First define your set of values, then the evaluation rules. Also explain informally what your rules are trying to accomplish. Values are those of the regular language, plus location values (as with references), plus mutable record values, whose components are location values: v ::= ... | l | {var id=l, ..., var id=l} l in Location Mutable record constructors just evaluate their arguments in l-to-r order, and then allocate N locations for the N component values, update the store with the locations initialized to the record components, and then return the record value containing the locations: E; Sigma |- e1 => v1; Sigma1 E; Sigma1 |- e2 => v2; Sigma2 ... E; Sigma(N-1) |- eN => vN; SigmaN {l1, ..., lN} does not overlap dom(SigmaN) -------------------- E; Sigma |- {var id1=e1, ..., var idN=eN} => {var id1=l1, ..., var idN=lN}; (SigmaN,l1=v1,...,lN=vN) Record projection works for both mutable and immutable records, but mutable records also dereference the location: E; Sigma |- e => {id1=v1, ..., idN=vN}; Sigma' 1 <= i <= N -------------------- E; Sigma |- (#idi e) => vi; Sigma' E; Sigma |- e => {var id1=l1, ..., var idN=lN}; Sigma' 1 <= i <= N (li=vi) in Sigma' -------------------- E; Sigma |- (#idi e) => vi; Sigma' Record assignment updates the contents of the assigned location: E; Sigma |- e1 => {var id1=l1, ..., var idN=lN}; Sigma' E; Sigma' |- e2 => v; Sigma'' 1 <= i <= N -------------------- E; Sigma |- (#idi e1 := e2) => (); (Sigma'',li=v) Sequences evaluate the argument expressions in order, ignoring the result value of the first: E; Sigma |- e1 => v1; Sigma1 E; Sigma1 |- e2 => v2; Sigma2 -------------------- E; Sigma |- (e1; e2) => v2; Sigma2 c) [7 pts Extra Credit]: Give the small-step eager-evaluation operational semantics for these constructs, in the style of lecture notes #15. Also explain informally what your rules are trying to accomplish. Mutable record constructors evaluate their arguments l-to-r, until they're a value, at which point they make a location for them in the store: --> -------------------- --> vi not a Location (forall i, 1 <= i <= N) li not in dom(Sigma) (forall i, 1 <= i <= N) -------------------- --> <(Sigma,l1=v1,...,lN=vN), {var id1=l1, ..., var idN=lN}> Record projection works for both mutable and immutable records, with mutable records also doing a dereference of the location: --> -------------------- --> 1 <= i <= N -------------------- --> 1 <= i <= N (li=vi) in Sigma [here "in" picks the right-most binding of li in Sigma] -------------------- --> Record assignment updates the contents of the location: --> -------------------- --> --> -------------------- --> 1 <= i <= N -------------------- --> <(Sigma,li=v), ()> d) [2 pts] Why would it be weird to define a lazy-evaluation version of this language? Because lazy evaluation and side-effects don't mix: one tries to relieve the programmer of the need to reason about order of evaluation (and in fact makes it very hard to do so), while the other depends critically on order of evaluation in order to determine the sequence of updates and reads of refs. e) [4 pts] Give the maximum safe subtyping rules over both mutable and immutable records (includes the largest number of subtyping relations). Also explain informally what your rules are trying to accomplish. Mutable records with more labels are subtypes of mutable records with fewer labels, but the types of the common components must be the same (the components are invariant, not covariant as in immutable records): M >= N -------------------- {var id1:tau1, ..., var idM:tauM} <= {var id1:tau1, ..., var idN:tauN} A mutable record is a subtype of the corresponding immutable record: -------------------- {var id1:tau1, ..., var idN:tauN} <= {id1:tau1, ..., idN:tauN} (By transitivity, together with the existing rule for subtyping over immutable records, we get the dropping of fields and generalizing of component types, so we don't have to encode it explicitly in this rule.) We keep the same rule for subtyping over immutable records as we had before: M >= N tau1 <= tau1' ... tauN <= tauN' -------------------- {id1:tau1, ..., idM:tauM} <= {id1:tau1', ..., idN:tauN'} ---------------------------------------------------------------------------- 9) [3 pts] Most languages allow functions to have multiple arguments, but only a single result. Scheme includes some additional special forms (which we didn't discuss in class) to allow a function to return multiple values. Why doesn't ML need such a construct? Because it has tuples and tuple pattern-matching, and one can get the effect of returning multiple values by returning a single tuple and then using pattern-matching to give names to the individual results. ---------------------------------------------------------------------------- 10) [4 pts] Some people claim that objects subsume closures, since there are functions embedded in the encoding of objects. To be able to fully simulate what can be done with first-class functions in Scheme or ML, what properties would be needed of an object-oriented language? In other words, explain how one can design an object-oriented language lacking first-class functions but still allowing all the first-class-function-based idioms of Scheme or ML. Give an example of such a simulation in a statically typed OO language, in a notation of your choosing. One would need the ability to declare a class nested within a method, so that the nested methods can access the variables of the lexically enclosing method. The implementation should also allow instances of the nested class to be returned from the enclosing method, preserving the values of the lexically enclosing variables in the process. Example: type Int2IntFn { method apply(int):int; } class AddN { method addN(x:int):Int2IntFn { class F extends Int2IntFn { method apply(y:int):int { return x + y; } (* x is free in F! *) }; return new F; } } val add1:Int2IntFn = new AddN().addN(1); val add2:Int2IntFn = new AddN().addN(2); add1.apply(3) --> 4 add2.apply(3) --> 5 ---------------------------------------------------------------------------- 11) Early in the course I argued for a pure reference-oriented data model (notes #4), in contrast to C's value-oriented data model (where pointers are one kind of value, and values are copied on assignment). a) [2 pts] How can we tell that Core ML uses a reference-oriented data model? Its orthogonal treatment of data, where any kind of value (including record, tuple, and union values) can appear in any variable or other value. There is no explicit pointer type, nor is there any copying in the operational semantics, just sharing of values. b) [3 pts] What aspects of Core ML's syntax, typing rules, and operational semantics would change if we wanted to support a C-style data model? The syntax would add pointer types and introduction and elimination rules for pointer values. The typing rules would just add type checking rules for the introduction & elimination rules. The operational semantics (for the version with memory & side-effects) would change to do copying as part of assignment, parameter passing, and result returning.