[Grace-core] Gradual typing with Dynamic return type

[Michael Homer]

On Tue, Sep 27, 2011 at 11:18 AM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
> This was originally to be a response to the other thread, but I found
> a broader issue in the process: does return type Dynamic conform to a
> static return type? It looks like there's a problem with either way
> around (worked through below).
James asked how C# works here. The paper is obscurely unhelpful, but
the compiler immediately rejects overriding a method with dynamic.
This code is a compile-time error:
  class Foo {
    public virtual String Meth() { return "Hello"; }
  }
  class DFoo : Foo {
    public override dynamic Meth() { return "test" ; }
  }
That would correspond to disallowing Dynamic as a conforming return
type in Grace, both statically and at runtime. That does weaken the
ability to add types gradually, though C#'s goals around its dynamic
type are different (interacting with inherently dynamically-typed
code, rather than gradual typing). So it may or may not be a
persuasive example for Grace, but it is something to think about.

The option of type-checking wrapper objects which throw an exception
when the type is unmatched is interesting, and I almost mentioned it
in the original message, but I'm not sure how it would work in
practice. In particular, there is a question around what it does to
object identity, and the effect that it has on pattern matching.

For pattern matches, the match can occur either on the type given by
the wrapper (i.e., the wrapper adopts the dynamic type implied by the
static type) or on the actual underlying object. In the case that it
matches the underlying object, pattern matching cannot be guaranteed
to be exhaustive. In the other, the static type information causes a
semantic change in the program. I believe there will be other subtle
issues that need resolution, but that is the clearest one.

On object identity (and egal), it seems to break them entirely. Either
object egality doesn't imply semantic equivalence, or "being the same
object" doesn't imply egality. It may be possible to work around that
for some definition of "well-behaved programs", but it seems pretty
fraught.
-Michael