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

[Andrew P. Black]

> On 28 Jul 2016, at 9:19, James Noble <kjx at ecs.vuw.ac.nz> wrote:
> 
> class Box[[T]](value) {
>  var contents : T is public = value
> }
> 
> def b = Box(1)
> b.contents := "Hello"
> print (b.contents)
> 
> but if we infer that we mean Box{{Number]] then this code will crash

Hence, that inference would be incorrect. 

On the other hand, if we defined (wait while I invent some syntax ...)

class box(value:T) forall T {
    var contents:T is public = value
}

then 

def b = box(1)

would indeed create a box that contained a field of type Number.   If we wanted a box that would hold things of a more general type, we could create it as

def b = box(1:Unknown)

You seem to be arguing inductively, from the particular to the general.  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.

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. 

	Andrew