[Grace-core] On Gradual Typing

[Michael Homer]

On Fri, Jul 19, 2013 at 10:21 AM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
> On Fri, Jul 19, 2013 at 9:40 AM, Kim Bruce <kim at cs.pomona.edu> wrote:
>> On Jul 17, 2013, at 2:56 AM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
>>> Let us consider the following completely statically-typed program:
>>> 1    object {
>>> 2        method x -> Done {
>>> 3            self.y
>>> 4        }
>>> 5    }
>>> Line 3 is clearly a static type error because there is no such method
>>> "y" on self.
>>>
>>> Now let us consider the following completely dynamically-typed program:
>>> 1    object {
>>> 2        method x {
>>> 3            self.y
>>> 4        }
>>> 5    }
>>> Line 3 is clearly a static type error because there is no such method
>>> "y" on self.
Discussion today has suggested an "is complete" annotation that can be
provided on object constructors, which the static checking dialect can
use to tell it to enforce this error. A stricter dialect could assume
it always; without the annotation "self" would be treated as
dynamically typed. I'm not sure whether that was fully agreed on, but
I am noting the idea here for everyone else.

A key benefit here is that "complete" and incomplete objects can
appear in the same module. Type annotations that are given on
parameters and variables will be enforced at run-time as usual,
whichever kind of object they're in and whatever state the typechecker
is in.

During the meeting I described four possible dynamic/static scenarios
based on what was defined at the time, varying by how the various
terms were interpreted and balanced:
1) The typechecker is always on, but omitted type annotations are
treated as Dynamic. "self" has an inferred type. You can't write
dynamically-typed code in this scenario.
2) There is an out-of-band switch that determines whether the
typechecker is enabled. There is a hard barrier at this switch for
gradually-typed code.
3) The typechecker is implemented as a dialect. Code in this dialect
is statically checked and code outside is not. There may be many
dialects with further layers of checking enabled. The entire module
has the same level of checking applied to it.
4) While the typechecker is always enabled, "self" is always treated
as dynamically-typed. You can't catch errors in self-requests
statically in this scenario.

I think the "is complete" version avoids the pitfalls of these
scenarios at the expense of a little extra work for partially-typed
programs that want to enforce checking of self-calls.
>> I would say that this is a static error, that should be caught at compile time in any Grace program, as it can in no circumstances be correct.  Thus, I personally would want an error (or at least a warning here) no matter how we are executing the program.
> The for loop is a bit of a red herring. Consider this example:
> 01    type Example = {
> 02        method go<E>(x : Iterable<E>) { ... }
> 03    }
> 04    def a : Example = object {
> 05        method go<E>(x : Iterable<E>) { print(E) } // Or a type test
> 06    }
> 07    def b : Dynamic = a
> 08
> 09    def l : List<Number> = generateNumberList
> 10    a.go(l)
> 11    b.go(l)
> Lines 10 and 11 almost certainly do distinguishably different things
> under inference, determined only by the static type of the receiver,
> because the generic parameter is retained. Perhaps that is ok; it is
> not the story that has been told so far.
Tim suggested that at runtime, omitted generic parameters are *always*
populated with Dynamic, while the static checker may infer types if it
wishes for its own use only. Kim agreed that this was acceptable to
him.

He apparently also has an answer to the question I had about blocks,
but I don't remember what it is. I think the general sense is that
extra arguments to blocks shouldn't be permitted. The static typing
I'm not sure about, but it is clear enough in the usual cases.
-Michael