\documentclass{article}
\usepackage{fullpage}
\usepackage{code}
\usepackage[override]{cmtt}
\usepackage{mathpartir}
\usepackage{versions}

\newenvironment{solution}{\textbf{Solution:}\\}{}
%\excludeversion{solution} % uncomment this line to not show solutions

\newcommand \pts[1]{(\textbf{#1} points)\ \ }

\newcommand \nextpage {\newpage Name:\underline{\hspace{3in}}\\}

\newcommand \bnfdef  {\mathrel{::=}}
\newcommand \alt     {\mathrel{|}}

\newcommand \arr {\rightarrow}

\newcommand \keyfont {\mathsf}
\newcommand \T {\tau}
\newcommand \A {\alpha}
\newcommand \G {\Gamma}
\newcommand \C {\cdot}
\newcommand \D {\Delta}
\newcommand \intty {\mathsf{int}}
\newcommand \unitty {\mathsf{unit}}
\newcommand \fnty[2] {{#1}\rightarrow {#2}}
\newcommand \lam[2] {\lambda{#1}.\ {#2}}
\newcommand \subst[3] {{#1}[{#2}/{#3}]}
\newcommand \tc[3]{{#1} \vdash {#2} : {#3}}
\newcommand \dom {\mathrm{Dom}}
\newcommand \tcF[4]{{#1};{#2} \vdash {#3} : {#4}}
\newcommand \Lam[2] {\Lambda{#1}.\ {#2}}
\newcommand \forallty[2] {\forall{#1}.{#2}}
\newcommand \kc[2] {{#1}\vdash{#2}}

\newcommand \primarr {\stackrel{\mathrm{p}}{\arr}}

\newcommand \muty[2] {\mu{#1}.{#2}}
\newcommand \roll[2]   {\mathsf{roll}_{#2}\ {#1}}
\newcommand \unroll[1] {\mathsf{unroll}\ {#1}}

\newcommand \sumty[2] {{#1}+{#2}}
\newcommand \Ac{\mathsf{A}}
\newcommand \Bc{\mathsf{B}}
\newcommand \Acons[1] {\Ac({#1})}
\newcommand \Bcons[1] {\Bc({#1})}
\newcommand \match[5] {\mathsf{match}\ {#1}\ \mathsf{with}\ \Ac {#2}.\
  {#3}\ |\ \Bc {#4}.\ {#5}}

\newcommand \Ref[1] {\mathsf{ref}\ {#1}}
\newcommand \refty[1] {{#1}\ \mathsf{ref}}

\newcommand \fix[1] {\mathsf{fix}\ {#1}}

\begin{document}
%\large

Name:\underline{\hspace{3in}}\\ \\
\centerline{\textbf{\Large CSE 505, Fall 2008, Final Examination}}
\centerline{\textbf{\Large 11 December 2008}}

\vfil
\textbf{\Large Please do not turn the page until everyone is ready.}
\vfil
\noindent Rules:
\begin{itemize}
\item The exam is closed-book, closed-note, except for one side of one
  8.5x11in piece of paper.
\item \textbf{Please stop promptly at 10:20.}
\item You can rip apart the pages.
\item There are \textbf{100 points} total, distributed among \textbf{6}
  questions.
\item The questions have multiple parts.
\end{itemize}
\vfil
Advice:
\begin{itemize}
\item Read questions carefully.  Understand a question before you
  start writing.
\item Write down thoughts and intermediate steps so you can get partial
  credit.
\item The questions are not necessarily in order of difficulty.
  \textbf{Skip around.}  In particular, make sure you get to all the problems.
\item If you have questions, ask.
\item Relax.  You are here to learn.
\end{itemize}

\nextpage

For your reference (page 1 of 2):

\[\begin{array}{rcl}
  e &\bnfdef& \lam{x}{e} \alt x \alt e\ e \alt c \alt \{l_1=e_1,
  \dots, l_n=e_n\} \alt e.l_i \alt \fix{e}\\
  v &\bnfdef& \lam{x}{e} \alt c \alt \{l_1=v_1, \dots, l_n=v_n\}\\
  \T &\bnfdef& \intty \alt \fnty{\T}{\T} \alt \{l_1:\T_1, \dots, l_n:\T_n\}
  \end{array}\]

\fbox{$e\rightarrow e'$ and $\tc{\G}{e}{\T}$ and $\T_1\leq\T_2$}
\begin{mathpar}
\infer{ }{(\lam{x}{e})\ v \rightarrow \subst{e}{v}{x}}
\and\infer{e_1\rightarrow e_1'}{e_1\ e_2\rightarrow e_1'\ e_2}
\and\infer{e_2\rightarrow e_2'}{v\ e_2\rightarrow v\ e_2'}
\and\infer{e\arr e'}{\fix{e}\arr\fix{e'}}
\and\infer{ }{\fix{\lam{x}{e}}\arr \subst{e}{\fix{\lam{x}{e}}}{x}}
\and\infer{ }{\{l_1=v_1,\dots,l_n=v_n\}.l_i\arr v_i}
\and\infer{e_i\arr e_i'}
      {\{l_1=v_1,\dots,l_{i-1}=v_{i-1},l_i=e_i,\dots,l_n=e_n\}
      \arr \{l_1=v_1,\dots,l_{i-1}=v_{i-1},l_i=e_i',\dots,l_n=e_n\}}

\end{mathpar}
\begin{mathpar}
\infer{ }{\tc{\G}{c}{\intty}}
\and \infer{ }{\tc{\G}{x}{\G(x)}}
\and \infer{\tc{\G,x:\T_1}{e}{\T_2}}
          {\tc{\G}{\lam{x}{e}}{\fnty{\T_1}{\T_2}}}
\and \infer{\tc{\G}{e_1}{\fnty{\T_2}{\T_1}} \\
            \tc{\G}{e_2}{\T_2}}
           {\tc{\G}{e_1\ e_2}{\T_1}}
\and\infer{\tc{\G}{e}{\fnty{\T}{\T}}}
        {\tc{\G}{\fix{e}}{\T}}
\and\infer{\tc{\G}{e_1}{\T_1}\\ \dots\\ \tc{\G}{e_n}{\T_n}\\
      \mbox{labels distinct}}
        {\tc{\G}{\{l_1=e_1,\dots,l_n=e_n\}}{\{l_1:\T_1,\dots,l_n:\T_n\}}}
\and\infer{\tc{\G}{e}{\{l_1:\T_1,\dots,l_n:\T_n\}} \\ 1\leq i\leq n}
          {\tc{\G}{e.l_i}{\T_i}}
\and\infer{\tc{\G}{e}{\T} \\ \T\leq\T'}{\tc{\G}{e}{\T'}}
\end{mathpar}
\begin{mathpar}
\infer{ }{\{l_1{:}\T_1,\dots,l_n{:}\T_n,l{:}\T\} \leq \{l_1{:}\T_1,\dots,l_n{:}\T_n\}}
\and\infer{ }
 {\{l_1{:}\T_1,\dots,l_{i-1}{:}\T_{i-1},l_i{:}\T_i,\dots,l_n{:}\T_n\}\leq
   \{l_1{:}\T_1,\dots,l_i{:}\T_i,l_{i-1}{:}\T_{i-1},\dots,l_n{:}\T_n\}}
\and\infer{\T_i\leq\T_i'}
        {\{l_1{:}\T_1,\dots,l_i{:}\T_i,\dots,l_n{:}\T_n\}
          \leq \{l_1{:}\T_1,\dots,l_i{:}\T_i',\dots,l_n{:}\T_n\}}
\\\infer{\T_3\leq\T_1\\
  \T_2\leq\T_4}{\fnty{\T_1}{\T_2}\leq\fnty{\T_3}{\T_4}}
\and\infer{ }{\T\leq\T}
\and\infer{\T_1\leq\T_2 \\ \T_2\leq\T_3}{\T_1\leq\T_3}
\end{mathpar}

\underline{\hspace{6in}}
\vspace{-0.5ex}
\begin{mathpar}
\begin{array}{rcl}
e &\bnfdef& c \alt x \alt \lam{x{:}\T}{e} \alt e\ e \alt \Lam{\A}{e} \alt e [\T]\\
\T &\bnfdef& \intty \alt \fnty{\T}{\T} \alt \A \alt \forallty{\A}{\T}\\
v &\bnfdef& c \alt \lam{x{:}\T}{e} \alt \Lam{\A}{e}
\end{array}
\and
\begin{array}{rcl}
\G &\bnfdef& \C \alt \G,x{:}\T\\
\D &\bnfdef& \C \alt \D,\A
\end{array}
\end{mathpar}
\fbox{$e\rightarrow e'$ and $\tcF{\D}{\G}{e}{\T}$}
\begin{mathpar}
\infer{e\arr e'}
      {e\ e_2\arr e'\ e_2}
\and\infer{e\arr e'}
       {v\ e\arr v\ e'}
\and\infer{e\arr e'}
      {e [\T]\arr e' [\T]}
\and\infer{ }{(\lam{x{:}\T}e)\ v\arr\subst{e}{v}{x}}
\and\infer{ }{(\Lam{\A}e)[\T]\arr\subst{e}{\T}{\A}}
\end{mathpar}
\begin{mathpar}
\infer{ }{\tcF{\D}{\G}{x}{\G(x)}}
\and\infer{ }{\tcF{\D}{\G}{c}{\intty}}
\and\infer{\tcF{\D}{\G,x{:}\T_1}{e}{\T_2}\\ \kc{\D}{\T_1}}
        {\tcF{\D}{\G}{\lam{x{:}\T_1}{e}}{\fnty{\T_1}{\T_2}}}
\and\infer{\tcF{\D,\A}{\G}{e}{\T_1}}
        {\tcF{\D}{\G}{\Lam{\A}{e}}{\forallty{\A}{\T_1}}}
\and\infer{\tcF{\D}{\G}{\!e_1}{\fnty{\T_2\!}{\!\T_1}}\quad
       \tcF{\D}{\G}{e_2}{\T_2}}
     {\tcF{\D}{\G}{e_1\ e_2}{\T_1}}
\and\infer{\tcF{\D}{\G}{\!e}{\forallty{\A}{\T_1}} \quad \kc{\D}{\T_2}}
          {\tcF{\D}{\G}{e [\T_2]}{\subst{\T_1}{\T_2}{\A}}}
\end{mathpar}

\nextpage

\underline{\hspace{6in}}

% recursive types and such
\begin{mathpar}
\begin{array}{rcl}
e  &\bnfdef& \dots \alt \Acons{e} \alt \Bcons{e} \alt (\match{e}{x}{e}{x}{e})
\alt \roll{e}{\T} \alt \unroll{e} \\
\T &\bnfdef& \dots \alt \sumty{\T_1}{\T_2} \alt \muty{\A}{\T}\\
v  &\bnfdef& \dots \alt \Acons{v} \alt \Bcons{v} \alt \roll{v}{\T}
\end{array}
\end{mathpar}
\fbox{$e\rightarrow e'$ and $\tcF{\D}{\G}{e}{\T}$}
\begin{mathpar}
\\
\infer{ }{\match{\Acons{v}}{x}{e_1}{y}{e_2}\arr \subst{e_1}{v}{x}}
\and\infer{ }{\match{\Bcons{v}}{x}{e_1}{y}{e_2}\arr \subst{e_2}{v}{y}}
\\\infer{e\arr e'}
          {\Acons{e}\arr\Acons{e'}}
\and\infer{e\arr e'}
          {\Bcons{e}\arr\Bcons{e'}}
\and\infer{e\arr e'}
          {\match{e}{x}{e_1}{y}{e_2}\arr\match{e'}{x}{e_1}{y}{e_2}}
\\
\infer{ }{\unroll{(\roll{v}{\muty{\A}{\T}})}\arr v}
\and\infer{e\arr e'}
      {\roll{e}{\muty{\A}{\T}}\arr \roll{e'}{\mu{\A}{\T}}}
\and\infer{e\arr e'}
      {\unroll{e}\arr \unroll{e'}}
\\
\infer{\tcF{\D}{\G}{e}{\sumty{\T_1}{\T_2}}
       \\ \tcF{\D}{\G,x{:}\T_1}{e_1}{\T}
       \\ \tcF{\D}{\G,y{:}\T_2}{e_2}{\T}}
      {\tcF{\D}{\G}{\match{e}{x}{e_1}{y}{e_2}}{\T}}
\\
\infer{\tcF{\D}{\G}{e}{\T_1}}{\tcF{\D}{\G}{\Acons{e}}{\sumty{\T_1}{\T_2}}}
\and\infer{\tcF{\D}{\G}{e}{\T_2}}{\tcF{\D}{\G}{\Bcons{e}}{\sumty{\T_1}{\T_2}}}
\and\infer{\tcF{\D}{\G}{e}{\subst{\T}{(\muty{\A}{\T})}{\A}}}
      {\tcF{\D}{\G}{\roll{e}{\muty{\A}{\T}}}{\muty{\A}{\T}}}
\and\infer{\tcF{\D}{\G}{e}{\muty{\A}{\T}}}
           {\tcF{\D}{\G}{\unroll{e}}{\subst{\T}{(\muty{\A}{\T})}{\A}}}
\end{mathpar}

\underline{\hspace{6in}}
\ \\
\ \\
Module Thread:
\begin{verbatim}
type t
val create : ('a -> 'b) -> 'a -> t
val join : t -> unit
\end{verbatim}
Module Mutex:
\begin{verbatim}
type t 
val create : unit -> t
val lock : t -> unit
val unlock : t -> unit
\end{verbatim}
Module Event:
\begin{verbatim}
type 'a channel 
type 'a event 
val new_channel : unit -> 'a channel
val send : 'a channel -> 'a -> unit event
val receive : 'a channel -> 'a event
val choose : 'a event list -> 'a event
val wrap : 'a event -> ('a -> 'b) -> 'b event
val sync : 'a event -> 'a
\end{verbatim}

\nextpage

\begin{enumerate}
  
\item \pts{20} Assume we have a typed programming language formally
  defined by a small-step operational semantics and a typing
  judgment.  Assume the appropriate Preservation and Progress Theorems
  hold for this language.  Consider each question below
  \emph{separately} and \textbf{explain your answers briefly}.
\begin{enumerate}
\item Suppose we change the operational semantics by adding a new
  inference rule.
  \begin{enumerate}
  \item Is it possible that the Preservation Theorem is now false?
  \item Is it possible that the Progress Theorem is now false?
  \end{enumerate}
\item Suppose we change the type system by adding a new inference rule.
  \begin{enumerate}
  \item Is it possible that the Preservation Theorem is now false?
  \item Is it possible that the Progress Theorem is now false?
  \end{enumerate}
\item Suppose we change the operational semantics by replacing one of
  the inference rules with a rule that is just like it except it has
  some additional hypothesis.
  \begin{enumerate}
  \item Is it possible that the Preservation Theorem is now false?
  \item Is it possible that the Progress Theorem is now false?
  \end{enumerate}
\item Suppose we change the type system by replacing one of
  the inference rules with a rule that is just like it except it has
  some additional hypothesis.
  \begin{enumerate}
  \item Is it possible that the Preservation Theorem is now false?
  \item Is it possible that the Progress Theorem is now false?
  \end{enumerate}
\end{enumerate}

\begin{solution}

\vspace{-1ex}
\emph{Note: Your instructor originally got part (b)i wrong.  Also,
  grading was fairly lenient on the explanations, but they had to make
  some sense.}

For the benefit of full, precise explanations, let's state
Preservation and Progress this way:
\begin{itemize}
\item Preservation: If ($\underbrace{\tc{\C}{e}{\T}}_A$ and
  $\underbrace{e\rightarrow e'}_B$), then
  $\underbrace{\tc{\C}{e'}{\T}}_C$.
\item Progress: If $\underbrace{\tc{\C}{e}{\T}}_D$, then $e$ is a value
    or $\underbrace{\mbox{there exists\ } e' \mbox{such that\ } e\rightarrow e'}_E$.
\end{itemize}

\begin{enumerate}
\item 
\begin{enumerate}
\item Yes, the new rule might produce an ill-typed term.  $B$
  is easier to satisfy, so $A$ and $B$ may no longer imply $C$.
\item No, more operational rules cannot make it harder to step.  $E$
  is easier to satisfy so $D$ still implies $E$.
\end{enumerate}
\item 
\begin{enumerate}
\item Yes, the new rule might let some term type-check that can take
  a step to produce a term that doesn't type-check.  $A$ is
  easier to satisfy, so $A$ and $B$ may no longer imply $C$ even
  though $C$ is also easier to satisfy.  As an example, suppose we
  have a rule give $(3+4)+()$ type $\intty$.  It can step to
  $7+()$, which does not type-check.
\item Yes, the new rules could allow a stuck term to type-check.
  $D$ is easier to satisfy, so $D$ may no longer imply $E$.
  For example, have a rule that gives $3+()$ type $\intty$.
\end{enumerate}
\item 
\begin{enumerate}
\item No, the changed rule is now harder to use, but any term allowed
  after a step was also allowed before the change.  $B$ is
  harder to satisfy, so $A$ and $B$ still imply $C$.
\item Yes, the changed rule might no longer apply, which
  could cause some expression to be stuck that was not stuck in the
  old language.  $E$ is harder to satisfy so $D$ may no longer
  imply $E$.
\end{enumerate}
\item 
\begin{enumerate}
\item Yes, the changed rule is now harder to use, so some term that
  used to type-check might no longer type-check, so if that term can
  be produced by a well-typed expression taking a step, Preservation
  no longer holds.  $C$ is harder to satisfy, so $A$ and $B$ may no
  longer imply $C$ even though $A$ is also harder to satisfy.
\item No, only fewer terms type-check when we add hypotheses, so the
  theorem still applies to all the terms that type-check
  after the change.  $D$ is harder to satisfy, so $D$ still implies $E$.
\end{enumerate}
\end{enumerate}
\end{solution}

\nextpage 

\item \pts{15} Consider a typed $\lambda$-calculus with recursive types,
  sum types, pair types, int, and unit.  Assume the language uses
  explicit roll and unroll coercions (not subtyping) for recursive types.

\begin{enumerate}
\item Define a type \verb|t1| for lists where each list element
  contains either one int or a pair of ints.  Use a sum type to tag
  list elements to distinguish these two possibilities.
\item Write a typed $\lambda$-calculus program of the form 
  $\fix{(\lam{sum {:} \mathtt{t1}\rightarrow\intty}
         {\lam{lst {:} \mathtt{t1}}
          {\underline{\hspace{6ex}}}})}$ for adding up all the
  integers in a list of type \verb|t1|.  For example, a list holding
  the pair (2,3) and the integer 7 would have a sum of 12.  Assume, of
  course, the expression language has addition.
\item Define a type \verb|t2| for a list where list elements
  \emph{alternate} between holding an int and a pair of ints, starting
  with an int.  That is, the first, third, fifth, etc. elements are
  ints and the second, fourth, sixth elements, etc. are pairs of ints.
  However, the list may have any number of total elements (including 0
  or an odd number).  Do not use a sum type for list \emph{elements}
  (although you still need sum types for the list itself).
\item Write a typed $\lambda$-calculus program of the form
  $\fix{(\lam{sum {:} \mathtt{t2}\rightarrow\intty} {\lam{lst {:}
        \mathtt{t2}} {\underline{\hspace{6ex}}}})}$ for adding up all
  the integers in a list of type \verb|t2|.  For example, a list
  holding the pair (2,3) and the integer 7 would have a sum of 12.
  Assume, of course, the expression language has addition.
\end{enumerate}

\begin{solution}
\begin{enumerate}
\item 
\[ \muty{\A}{\sumty{\unitty}{((\sumty{\intty}{(\intty*\intty)}) *
    \A)}} \]
\item 
\begin{verbatim}
  fix (lambda sum : t1 -> int. lambda lst : t1.
         match unroll lst with
            A x -> 0
            B x -> (match x.1 with
                      A y -> y
                    | B y -> y.1 + y.2)
                   + sum x.2)
\end{verbatim}
\item 
\[ \muty{\A}{\sumty{\unitty}{(\intty *
    (\sumty{\unitty}{((\intty*\intty)*\A)}))}} \]
\item 
\begin{verbatim}
  fix (lambda sum : t1 -> int. lambda lst : t1.
         match unroll lst with
             A x -> 0
           | B x -> x.1 + (match x.2 with
                             A y -> 0
                           | B y -> (y.1.1 + y.1.2) + sum y.2))
\end{verbatim}
\end{enumerate}
\end{solution}

\nextpage 

\item \pts{20} In this problem you will use CML to implement futures.
  Futures have this interface:
\begin{verbatim}
type 'a promise
val future : (unit -> 'a) -> 'a promise
val force : 'a promise -> 'a
\end{verbatim}
  Recall a future runs in parallel and \verb|force| blocks until the
  result is ready.  It \emph{is} permissable to call \verb|force| with
  the same promise multiple times; if the result has already been
  computed it is simply returned immediately.

\begin{enumerate}
\item Provide an implementation of the interface above in CML\@.  Do
  not use mutation.  Remember to include the definition of 
  \verb|type 'a promise|.
\item Consider an extended interface with:
\begin{verbatim}
val force_any : 'a promise list -> 'a
\end{verbatim}
Extend your implementation to provide this function.  It should block
only until one of the promises in the list is ready.  If more than one
is ready, it can return the result of any of the ready ones.

\end{enumerate}

\begin{solution}
\begin{enumerate}
\item 
\begin{verbatim}
type 'a promise = 'a channel

let future th =
  let c = new_channel() in
  let rec loop v = sync (send c v); loop v in
  ignore(create (fun () -> loop (th ())) ());
  c

let force p = sync (receive p)
\end{verbatim}
\item
\begin{verbatim}
let force_any ps = sync (choose (List.map receive ps))
\end{verbatim}
\end{enumerate}
\end{solution}

\nextpage 

\item \pts{15} Consider a class-based OOP language like we did in class.
  Suppose it has abstract methods.  Recall that a class that defines
  or inherits abstract methods cannot have instances unless all
  abstract methods are overridden.  
  
  In this problem, we consider a bad idea for a new language feature:
  If class $C$ inherits abstract method $m$, then $C$'s definition can
  include \verb|remove| $m$ to mean instances of $C$ do not have
  method $m$.  This allows us to create instances of $C$ unless there
  are other abstract methods that are neither overridden nor
  ``removed.''

  \begin{enumerate}
  \item Explain why this new feature is unsound if subclasses are
  subtypes.  Give an example with a superclass, a subclass, and
  ``client code'' that makes an instance of the subclass.  Your
  example should not require any concrete methods in the superclass.
  
  \item Explain why this new feature is unsound even if subclasses that
  remove methods are not subtypes of their superclasses.  Give an
  example with a superclass, a subclass, and ``client code'' that
  makes an instance of the subclass.
  \end{enumerate}

\begin{solution}
\begin{enumerate}
\item With subclasses as subtypes, a subclass needs to have every
  method that the superclass has.  Even though the superclass does not
  give a definition for an abstract method, its type assumes the
  method exists.  Hence this program type-checks but gets stuck:
  \begin{verbatim}
  class B { abstract unit m(); }
  class C extends B { remove m }
  ((B)new C()).m();
  \end{verbatim}
\item When we type-check methods in the superclass, we assume all
  methods exist as provided by the superclass' type.  This includes
  abstract methods, which thanks to late-binding will exist whenever a
  method in the superclass is called.  But with our new feature, we
  are no longer required to define these methods, as in this example:
  \begin{verbatim}
  class B { abstract unit m();
            unit n() { self.m(); }
          }
  class C extends B { remove m }
  (new C()).n();
  \end{verbatim}
\end{enumerate}
\end{solution}

\nextpage 

\item \pts{15} This problem considers the code below in a
  class-based OOP language.  Assume classes \verb|A|, \verb|B|,
  \verb|C|, and \verb|D| have no subclasses except those shown.
\begin{verbatim}
  class A {}
  class B extends A {}
  class C extends B {}
  class D {
     int m(A x, A y) { return 1; }
     int m(A x, B y) { return 2; }
     int m(A x, C y) { return 3; }
     int m(B x, A y) { return 4; }
     int m(B x, B y) { return 5; }
     int m(B x, C y) { return 6; }
     int m(C x, A y) { return 7; }
     int m(C x, B y) { return 8; }
     int m(C x, C y) { return 9; }
     int foo(A a, C b) {
        return self.m(a,b);
     }
  }
\end{verbatim}
 
\begin{enumerate}
\item Suppose our language has multimethods.  What are the possible
  values that a call\\ \verb|(new D()).foo(e2,e3)| could return?  
\item Suppose our language has static overloading.  What are the possible
  values that a call\\ \verb|(new D()).foo(e2,e3)| could return?  
\item How, if at all, do your answers change if subclasses of \verb|D|
  might exist but subclasses of \verb|C| do not? 
\item How, if at all, do your answers change if subclasses of \verb|C|
  might exist but subclasses of \verb|D| do not? 
\end{enumerate}

\begin{solution}
\begin{enumerate}
\item It could return 3, 6, or 9.  At run-time, \verb|a| could be
  bound to an instance of \verb|A|, \verb|B|, or \verb|C| whereas
  \verb|b| will be bound to an instance of \verb|C|.  Since
  method-lookup uses these run-time classes, the unique best match
  will depend on the value bound to \verb|a|.
\item It will return 3.  The method-lookup is resolved using types
  \verb|A| and \verb|C| for the first and second arguments respectively.
\item In this case, neither answer changes since the receiver is
  something with run-time class \verb|D|.  (The answer could be
  different if we knew only that the receiver had type \verb|D|, which
  is actually what your instructor meant to ask.)
\item In this case, neither answer changes.  We have the same 9
  methods named \verb|m|.  The new possibilities are \verb|a| or
  \verb|b| could be bound to a suclass of \verb|C|.  With
  multimethods, that will result in the answer 9 since this will
  require the fewest subsumptions.  With static overloading, that will
  result in the answer 3 since the run-time classes remain irrelevant.
\end{enumerate}
\end{solution}

\nextpage 

\item \pts{15} This problem considers a typed language with support for
  bounded parametric polymorphism, i.e., types of the form
  $\forall\alpha<\T_1.\ \T_2$.

\begin{enumerate}
\item The System F typing rule for type application:
\[\infer{\tcF{\D}{\G}{e}{\forallty{\A}{\T_1}} \quad \kc{\D}{\T_2}}
          {\tcF{\D}{\G}{e [\T_2]}{\subst{\T_1}{\T_2}{\A}}}
\]
is no longer appropriate because (1) $e$ does not have a bounded
polymorphic type and (2) $\T_2$ is not checked against a bound.
Replace this typing rule with a more appropriate one.

\item Suppose our language has addition, records with mutable fields, and
  $e_1; e_2$ for sequencing.  Then this term type-checks:
\[ \lam{x {:} \{l_1{:}\intty, l_2{:}\intty\}}{((x.l_1 := x.l_1 +
  x.l_2);\; x)} \]
  Use bounded polymorphism to give a value $v$ that has the same
  run-time behavior as this term but has a much more general type.
  Use the syntax $\Lambda\A<\T.e$ to create a bounded
  polymorphic expression.

\item Using the $v$ you defined in part (b), give a $\T$ and $v_2$
  such that $v\ [\T]\ v_2$ type-checks (using the rule you defined in
  part (a) and the rule for function application).  Choose a $v_2$
  that takes advantage of the subtyping allowed by bounded polymorphism.
  
\item What is the type of the expression ($v\ [\T]\ v_2$) in your
  answer to part (c)?  You do \emph{not} need to write down a typing
  derivation.
  
\end{enumerate}

\begin{solution}
\begin{enumerate}
\item 
\[ \infer{\tcF{\D}{\G}{e}{\forallty{\A<\T_3}{\T_1}} \quad \kc{\D}{\T_2<\T_3}}
          {\tcF{\D}{\G}{e [\T_2]}{\subst{\T_1}{\T_2}{\A}}}
\]
\item 
\[\Lambda\A< \{l_1{:}\intty, l_2{:}\intty\}.\ \lam{x {:} \A}{((x.l_1 := x.l_1 +
  x.l_2);\; x)} \]
\item (One example)\\ Let $\T$ be 
$\{l_1{:}\intty, l_2{:}\intty, l_3{:}\intty\}$ and $v_2$ be
$\{l_1=7, l_2=8, l_3=9\}$.
\item (Answer depends on part (c))\\
$\{l_1{:}\intty, l_2{:}\intty, l_3{:}\intty\}$
\end{enumerate}
\end{solution}

\end{enumerate}
\end{document}
