[Grace-core] Gradual typing with Dynamic return type

[James Noble]

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