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

[Vitek, Jan]

Not necessarily — some gradual type systems strive very hard to prevent the program from failing due to the addition of types (the example is Dart or Hack).

Other gradual type systems accept that some fine dynamic programs will fail when type annotations are added (Racket).

In the case of Thorn and StrongScript, we let the programmers choose. Like types will never cause runtime failures, while concrete types may.

-j


Jan Vitek, Professor 
Computer Science, 
Northeastern University

> On Jul 28, 2016, at 5:26 PM, Andrew P. Black <black at cs.pdx.edu> wrote:
> 
> Hi James,
> 
> Why do you say that inferring type parameters (which I think is what you mean by “populating the retained generic parameters via inference”) changes the operational semantics?
> 
> Yes, it does this when you reflect on the available type information.   In that sense, α-renaming changes the operational semantics too, since you can observe the change in variable name and change behavior accordingly.
> 
> Yes, it also does this if we want “precise exceptions”, because inference will potentially replace a NoSuchMethod Exception at some point in a program with a TypeError at an earlier point.   
> 
> I think that we have agreed that these are both OK things to do.
> 
> I believe that the case you are worried about is when type inference creates a TypeError in a program that would not have raised a NoSuchMethod Exception (e.g, because the “bad” value is never used).  Is that right?   Arn’t such errors part of the cost of doing business with types?
> 
> 	Andrew
>