[Grace-core] Should Grace abandon "gradual typing" for "like typing"?

[James Noble]

Hi all

So we've all been wondering what to do about gradual types in Grace,
what the semantics should be, how to implement them, etc, with the
easy cases being unsound and the sound cases not easy. We talked
about this with Tim & Laurie yesterday, I also talked with Jan at the
ESOP PC workshop etc, and he said "you should do what we did in Thorn".

I think he's right. 

To quote from their POPL10 paper: 

> We introduce a novel intermediate point, dubbed a “like type,” between dynamic and compile-time checked static types. For each type C, there is a type like C. Uses of variables of type like C are checked statically and must respect C’s interface. However, at run-time, any value can flow into a like C variable and their con- formance to C is checked dynamically.

this is exactly the semantics I was arguing for yesterday: you check types dynamically as much as you can, but e.g. if you have a type List[Number] 
and you get passed a List[Unknown] then that type check will pass, but the
code will crash later when you pull a String out of the List.  

StrongScript uses like types by default, and also (traditional) concrete types
(written !T) that don't match actual types Unknown in objects. 

I think this can work, and will hopefully be easy to implement even avoiding the "Groovy Effect" (more type declarations -> slower code).

comments?

PS: 

Concrete Types for TypeScript - ECOOP15
Gregor Richards, Francesco Zappa Nardelli, and Jan Vitek

Integrating typed and untyped code in a scripting language - POPL10
Tobias Wrigstad, Francesco Zappa Nardelli, Sylvain Lebresne, Johan Östlund, and Jan Vitek.

Thorn—robust, concurrent, extensible scripting on the JVM - OOPSLA09
Bloom and a cast of thousands.

for Gracies, the papers are all in BackgroundPapers... 

James