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

[Vitek, Jan]

The one thing that we have not explored is gradual typing for Generics with — like types are fine, but to get the same benefit out of concrete types (i.e. no wrappers) you have to avoid erasing the generic type information (a la C#) and perhaps more. 

Not being a fan of generics I have tried to see how far we can go without having to deal with them.

-j


Jan Vitek, Professor 
Computer Science, 
Northeastern University

> On Jul 27, 2016, at 2:11 PM, 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