[Grace-core] On Gradual Typing

[Michael Homer]

On Thu, Jul 18, 2013 at 1:14 PM, Andrew P Black
<andrew.p.black at gmail.com> wrote:
> Thanks for opening this dissuasion, Michael.
>
>
> On 17 Jul 2013, at 02:56 , Michael Homer wrote:
>
>> So far, the conception of how gradual typing works in Grace has been
>> that the typechecker is always there, but that by using "Dynamic" or
>> omitting the annotations you can get dynamically typed code that the
>> typechecker doesn't do anything with.
>
> That wasn't how it we imagine it at least at some time in the past — we imagined a lever on the side of the IDE that told it how to
> respond to type errors.
So this is essentially the dialect option. The language itself needs
to have some defined semantics still.
> Michael, what is your first problem?   Some code requests y on self, and the compiler is able to prove that self don't (yet) have a y.   What's the issue?  Whether the system should issue a warning?  Whether it should let the student run the program?   Or what?
In a statically-typed language, this must be a static error. In a
dynamically-typed language, it is not an error (until you run it). In
Grace, because the two coexist at once, it (according to the story I
gave) must be an error notwithstanding that the program is meant to be
dynamically-typed. Even though the author has different intentions
when writing them, the two programs have the same source code, so
there's no way to tell them apart.

An out-of-band lever is one way of dealing with that. The "gradual"
story - where you start with a fully dynamic program, and add types to
it piecewise - still has a problem, though, because your program will
break as soon as you switch the typechecker on. There's a red-line
change there, rather than gradual.

There are multiple ways of addressing all of these points. I have
semi-suggested some of them in the first message, but the important
thing is that they actually be resolved and fixed somehow.
-Michael