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

[James Noble]

Hi Éric

On 29/07/2016, at 11:44AM, Éric Tanter <etanter at dcc.uchile.cl> wrote:
> 
> On the question of gradual vs. inference, you might find Garcia & Cimini's paper on “principal type schemes for gradual programs” (POPL’15) quite illuminating.

thanks for pointing that out. I know some of Ron's work, but hadn't focussed on this one (perhaps because it seems overly functional).

from a brief look at the first page, it says

> 	• The key insight underlying the design is to only allow fully static types to be implicit: gradual types, in our approach, must originate in the program text.

which perhaps is where Jeremy's (?) quote came from - having both type inference and gradual types share the same syntax is hard.   So far we've 
picked the opposite design choice: gradual types are implicit so inferrred types would have to be explicit. 

That would mean e.g. we could address the Box example in the same way as Java's "diamond" <>  -- we could have an analogous "box" [[]] I guess -- which means infer a static type and use it to populate dynamic types.

So Box[[]](1) would presumably correspond to Box[[Number]](1),
while Box(1) would correspond to Box[[Unknown]](1)...

Or, as I think that paper suggests, we could do it the other way around.
Box(1) has types inferred, corresponding to Box{[Number]](1)
programmers have to write Box[[Unknown]](1) to get the gradual type.

James