[Grace-core] Gradual typing with Dynamic return type

[James Noble]

Thinking this over...

On 27/09/2011, at 11:18 AM, Michael Homer wrote:

> statically-typed code has no real type-safety
> guarantees at runtime if it's mixed with Dynamic

Yes, that's probably right. Or more than probably, it's got to be right. 

> There's no way for the code from above to raise an error
> unless every assignment or invocation is accompanied by a runtime
> check


not quite sure about that though...

>  var bst : BST
>  ...
>  var bst' : BST | None := bst.right

So I don't think you should have to check every assignment or method call -
but you will have to check every cast *from* Dynamic to some non-dynamic type.
(obviously you don't have to check going the other way)

Now say we have an EvilBST 

type EvilBST = {
   left -> Dynamic
   right -> Dynamic
   value -> Dynamic
 }

var x  // implicitly Dynamic
x := EvilBST.new    // "casts" or "converts" EvilBST to Dynamic. No check needed.

bst := x  // "casts" from dynamic to BST. Need to check here.
bst.right  // casts from dynamic to BST. Need to check here

but if there aren't any method sends that don't involve conversions out
of Dynamic, I don't think we need to check anything.

Then the issues are really about efficiency.
I think much of the complexity of Racket's 
Typed Modules (DLS 09?)  and why classes
aren't supported in Typed Scheme is because -  to 
be efficient you have to wrap dynamic objects with
adapters that do the typechecking...  

Thorn gets around this by having "normal" types - 
that *aren't* compatible with Dynamic, and then
"like T" types which are statically checked, well, like T,
as regards method requests, but they are always 
dynamically checked. So incorporating something
like that would be another option - if not like types,
then perhaps exact types can't be cast to dynamic...

But then, to use Andrew's terminology, if an implementation
wants to support the GWBush or EdMorrow semantics
(try and run basically ignoring all type annotations)
then it needs to be able to cope with anything anyway.
That probably does need checks on all calls as well
as "casts" - because things like this need to run 

  3 + Cucumber.new  // to quote Mads Torgersen, compile & print a runtime error

or run this without reporting any errors

 def perlis : BST := "Strong Typing"
 print(perlis + " is a crutch for weak memories") 

an implementation that can do that doesn't need to worry about Dynamic..

James