[PL-sem-jr] Traits references; follow-ups

[Richard Cobbe]

On Thu, Aug 11, 2005 at 09:26:26PM -0400, Richard Cobbe wrote:
> As promised, here are the BibTeX entries for the papers I covered today.
> 
> First, though, one or two follow-up items that occurred to me after I
> finished the talk.
> 
> 1) Felix asked why the method exclusion form, written T - (m : tau),
>    requires the programmer to state the type of the removed method.  We
>    agreed that this was unnecessary for the static semantics, and I
>    theorized that this was necessary to make the soundness proof work.
> 
>    Turns out it's required for the *dynamic* semantics, which I didn't
>    write out.  The reduction relation on traits maps trait values 
>    <| M; theta; S |> to trait values; remember that theta is a row type
>    containing the types of all required fields and methods.
> 
>    In evaluating the method exclusion, we have to move the excluded
>    method and its type into this row type.  And this requires having the
>    type in the program text---unless you want to re-type-check the
>    method body, at run time (or at least at link time).

(Sorry; forgot to put this in the first message.)

Another alternative, which Fisher & Reppy acknowledge in a footnote, is
to have the programmer annotate each function definition with its
return type.  They also raise the more remote possibility of addressing
this by changing the way they evaluate traits, but they don't provide
any details on that.

Richard