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

[Andrew P. Black]

Interesting proposal, I think, but I don’t understand how this is different from what we have now.  The short summary is a bit too cryptic, and I don’t have the time right now to study the papers.

Can you summarize the changes that you are proposing to the current Grace semantics?

	Andrew

> On 27 Jul 2016, at 5:11, James Noble <kjx at ecs.vuw.ac.nz> wrote:
> 
> 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
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core