[Grace-core] On Gradual Typing

[Kim Bruce]

A few comments interspersed:

On Jul 24, 2013, at 5:20 PM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:

> 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.

I'm not sure I would put this quite as strongly.  As I tried to point out in our meeting, Grace requires variable declarations.  That doesn't seem to stop dynamically typed code.  It also is not much of an impediment for a programmer doing exploratory coding.  The system provides a warning or error if the declaration is omitted and the programmer puts in a declaration to show they really meant for it to be a new variable, not a typo or other mis-remembering of an existing name.

If an object has type dynamic, then one can send any message with no warnings.  The issue here is with self.

If inside the body of an object/class definition, you write self.m and there is no m in the definition, then I would like the programmer to be warned about this.  If you are in "macho" dynamic programming mode, then just ignore the warning.  Otherwise, you can add a statement like Andrew's suggested "requires m(...)" statement that tells the system that you will eventually define (or inherit) such an m.  I personally think of this as being similar to the "var" declaration that ensures that you really meant to do this and it is not a typo or oversight.  In a well-developed IDE, it would of course offer to inset this code for you.  As usual, in dynamic-typing mode one would not need to put in the type info, but one would have to indicate the number of parameters that such a method has, either by putting in parameter names or underscores.

While this is more than Python programmers have to do now, our requirement of inserting var declarations also asks more.
> 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 dislike this scenario as it defeats the purpose of static type checking and will not pick up all reasonable type errors even when an object is fully annotated.
> 
> 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'd rather have the default be the opposite so the default would be to catch the errors unless you decide to bypass it.

I'm assuming this would work out to be that if an unknown method was requested of self then either the object/class would have to be labelled as "incomplete" or appropriate "requires" statements would need to be attached.  I could live with this.  This seems as though it would allow a mix of dynamic and statically typed code.

>>> 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.

I think this is probably the only reasonable solution to this issue unless something occurs to us later.  Type parameters are clearly a place where there is a wide gap between practices in statically and dynamically typed code.
> 
> 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.

That is correct.  Essentially what Tim outlined is what I prefer.  The arity must match up (just as it must for other method requests).  I see no reason to have an uber-Block type that is a supertype of them all.

> -Michael
> 
> _______________________________________________
> Grace-core mailing list
> Grace-core at cecs.pdx.edu
> https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core