CMSC 221/321
Homework set 7
Due: midnight, Tuesday, November 22

Template code for Hw 7.1 and 7.2 is available in the tarball hw7.tgz.
This code standardizes the abstract syntax to be used in
ptfunsyntax.sml. A standard definition of environments as alists
is given in env.sml.


7.1 [25]: Add recursive types and polymorphism the type checker from
Hw 6.1, producing a full type checker for PTFun, following the
specifications given in Figures 5.2 (abstract syntax) and 5.8 (typing)
in Lecture 10. 

Note that Fst, Snd, Inl, and Inr are treated as predefined variables
with polymorphic types, but Fold and Unfold still have to be treated
as special forms of expressions.  [You will have to modify or add
around 30 lines of code in ptfuntype.sml.]


7.2 [10]: Add the polymorphism constructs to the evaluator from Hw 6.2.
If you did not do so for extra credit on Hw 6.2, add support for the
polymorphic constructs TFun and TApp to your big-step evaluator for
PTFun.  [This should only require about 5 lines of added code in
ptfuneva.sml.]


7.3 [25] Define a CK machine for the full PTFun language based on the
small-step semantics given in Lecture 10, Figure 5.7.


7.4 [25 optional extra credit]. Show how to type states of the CF
machine from Hw 7.3. This involves typing stacks, which in turn
involves typing frames. Types of frames and stacks are pairs of types
(τ1,τ2), where τ1 would be the type of the value being "received" by
the frame (or stack), and τ2 is the type being delivered by the frame
to the next frame in the stack, if any.  For stacks, the second type
will be unchanging, and will be the type of the original expression.
The first type τ1 for a stack will agree with the corresponding 
control expression.

Thus, during the CK evaluation of an expression e, where ⊦ e: τ,
all states will be of the form 

    (e', s)

where ⊦ e': τ' and ⊦ s : (τ', τ).

For the purpose of typing frames and stacks, you may have to add 
additional type information to the frames.

State a Preservation Lemma for the typed CK machine, and prove 3
cases in the proof. [Is the proof inductive?].