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

[Éric Tanter]

Hi all,

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.

It clarifies that gradual is not (essentially) about plugging question marks whenever there are no annotations, but that gradual typing is about reasoning with _imprecise_ type information. How the imprecision comes about (whether by explicit ascription of unknown, or by missing annotation) is a separate question. In their design, imprecision is introduced through explicit ascriptions (like in Andrew’s example), and static inference never introduces additional imprecision.

Cheers,

— Éric