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

b) [3 pts] val f: ('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]

b) [3 pts] type G = rec t = {a:int, b:t}

c) [3 pts] type H = [Frob:int, Fribble:string, Qux:bool->bool]

d) [3 pts] type F = forall a. (a -> (forall b. (a*b -> b)))

-----------------------------------------------------------------------------

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)

b) [3 pts] 'a * ('b -> 'c)  ==  ('d * 'e) -> 'f

c) [3 pts] ('a -> 'b) * 'b  ==  (int -> ('c * string)) * (bool * 'd)

d) [3 pts] 'a * 'c  ==  ('b -> 'c) * 'a

e) [2 pts] If during type inference, two types don't unify, what does it mean?

----------------------------------------------------------------------------

4) [3 pts] What is the difference between forall and Lambda?  Give an
example illustrating the difference.

----------------------------------------------------------------------------

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}

b) [3 pts] [a:int, b:bool] <= [a:num, b:Object, c:int]

c) [3 pts] (int->Object) -> (num->string)  <=  (num->string) -> (int->Object)

d) [3 pts]
   ({x:int, y:int, z:int} -> [i:int])  <=  ({x:int, y:int} -> [i:int, j:int])

----------------------------------------------------------------------------

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);
(* new Foo(3) just builds an instance of Foo whose x instance variable
is initialized to 3; you don't need to implement constructor
functions. *)

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");

c) [4 pts]

class Qux extends Baz[bool] {
  method baz(arg:Foo):Foo { return self; }
}
val qux:Qux = new Qux(5, true);

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.

e) [3 pts] Is Baz[bool] a subtype of Baz[Object]?  Explain why or why not.

----------------------------------------------------------------------------

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);

-----------------------------------------------------------------------------

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.

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.

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.

d) [2 pts] Why would it be weird to define a lazy-evaluation version
of this language?

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.

----------------------------------------------------------------------------

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?

----------------------------------------------------------------------------

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.

----------------------------------------------------------------------------

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?

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?