[Grace-core] Gradual typing with Dynamic return type
James Noble
kjx at ecs.vuw.ac.nz
Tue Sep 27 03:18:57 PDT 2011
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
More information about the Grace-core
mailing list