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

[James Noble]

On 29/07/2016, at 5:04AM, Andrew P. Black <black at cs.pdx.edu> wrote:
> 
>> but if we infer that we mean Box{{Number]] then this code will crash
> 
> Hence, that inference would be incorrect. 

fine. But that inference is also pretty straightforward: 
I don't see how to create an inference rule that does not infer 
the generic type of Box there as Number. 

> def b = box(1:Unknown)

so we now have to officially "cast" 1 to Unknown to get dynamically typed behaviour?  

> You seem to be arguing inductively, from the particular to the general.  

I'm trying to argue the general case: both type inference and gradual/option/dynamic/like typing work by defining
what happens if types are not supplied.  The catch is that 
the bindings that type inference (on one side) and gradual etc
typing work are difference.

You could think of gradual/dynamic etc typing as a simple rule:
"always infer the Unknown (i.e. dynamic) type" 
That's the rule we've used so far.

10.1.4: ... If a declaration is not annotated, then the type of the declared name is implicitly Unknown. In addition, omitted type arguments are replaced by Unknown. 

The advantage of this definition is that removing a type annotation does not affect correctness (modulo reflection/cactching errors etc)

> Clearly some type inference algorithms will cause unwanted type errors.  Others will not, but will provide no useful information.  The interesting question to me is whether there are algorithms in between, that provide some useful information without generating inappropriate errors.  Exhibiting an algorithm in the first category doesn’t help to answer that question.

Before we can pick a type inference algorithm, we need to sort out the 
relationship between inferred types and omitted/Unknown/dynamic types.
Again: you can think of the current design as an "inference" algorithm
that always infers Unknown. 

> It may be that the programmer needs to provide more information about their intentions in the language syntax to get a useful inference algorithm.  The above “forall” syntax, stolen from Emerald, is just an example of something that  might help. 

Something like that is a possibility. The question is: how much "dynamic"
(especially implicit dynamic) behaviour are we willing to sacrifice, and 
how much more complex does that make the overall model.

J