[Grace-core] Gradual typing with Dynamic return type
James Noble
kjx at ecs.vuw.ac.nz
Mon Oct 10 05:08:44 PDT 2011
Returning to Michael's message:
> 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.
yep, I think this is what Typed Racket does - and also (presumably)
the Igarashi paper with the banana casts...
> In particular, there is a question around what it does to
> object identity, and the effect that it has on pattern matching.
right. For identity, it would have to be transparent -
hopefully that shouldn't be a problem, although it would
slow things down (unless one got sneaky with object encodings?)
> 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.
Hmm - can you give an example.
It seems to me, once you've got type Dynamic,
you're unable to be exhaustive in any case -
you're going to require a dynamic type test somewhere,
and presumably that test can fail.
> 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.
static type information may cause a semantic change
to an "incorrect" program (for some definition of incorrect:
presumably one that fails with a type error)
if I've an object with a method m returning dynamic
and I somehow wrap it to {m->number} presumably
m not returning number is a type error...
the real problem with wrapping is that
- it seems unpredictable & complex & slow
- one of our principles was "no automatic conversions" :-)
it's not clear it does the right thing
say we have o : { m -> Dynamic }
and run
match o
case { mNumber : { m -> Number } -> mNumber.m }
case { mDynamic : { m -> Dynamic } -> print "m Dynamic!!" }
this way round, presumably the first case would match, the object would be wrapped.
but if we put the cases the other way around
match o
case { mDynamic : { m -> Dynamic } -> print "m Dynamic!!" }
case { mNumber : { m -> Number } -> print( mNumber.m + 3) }
then the first case will *always* match anything (or rather, anything
with a message m - even if o actually has the type { m -> None }
the number case will never run.
This would be the same behavior as
match o
case { mDynamic : { m -> Any } -> print "m Any!!" }
case { mNumber : { m -> Number } -> print( mNumber.m + 3)}
anything with an m message prints "m Any"
Reversing the cases, an object with type {m->Any}
(or {m->Object} would *not* match the first case;
but again an object with type {m->Dynamic}
presumably *would* match - but again matching contravariantly,
so needed to be wrapped...
match o
case { mNumber : { m -> Number } -> print( mNumber.m + 3)}
case { mObject : { m -> Any } -> print "m Object!!" }
thinking about implementation & wrapping, it's possible
that Java-stype encoding of return types into method names
may be a way to handle this. First do a type-speciifc lookup;
and if that fails, *then* check for the dynamic case...
J
More information about the Grace-core
mailing list