[Grace-core] On Gradual Typing

[Michael Homer]

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.
>
> 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.
01    method new {
02        object {
03            method x {
04                self.y
05            }
06        }
07    }
08    object {
09        inherits new
10        method y { print "OK" }
11        self.x
12    }
This program is dynamically correct, but from the typechecker's
perspective lines 2-6 are the same. It is possible to figure it out in
this case, although not generally without whole-program analysis.
>> In statically-typed code, though, what does that mean? If I write
>> 1    for (someList) do { v : X -> print(v) }
>> then that must (because we have gradual typing) mean the same thing as
>> the dynamically-typed case, regardless of whether we know the type of
>> the method. That rules out inference of the parameter. So in your
>> statically-typed code, this loop is actually
>> 1    def someList : List<Number> = generateNumberList(5)
>> 2    for<Number> (someList) do { v : Number -> print(v) }
>> This seems unwieldy, but perhaps it is acceptable to the people who
>> are concerned with that. Internal iterators do not have this problem,
>> although the general issue still stands.
>
> I have more to say about blocks below, but I believe this is a case where local type inference can be effective (when in static checking mode).  Inferring the Number type parameter is easy given the type annotation on v.
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.
>> Secondly, that given all of this, anywhere that type inference is
>> required is a significant problem. With the typechecker necessarily
>> optional, it isn't possible for it to modify the behaviour of the
>> program, but it would need to do so to allow inference to occur.
>> Inferring out of blocks is one thing, but inferring generic parameters
>> is simply not possible. Variants of the rule where inference only
>> occurs for statically-typed code cause spooky action at a distance,
>> where a new type annotation in one part of the program causes a
>> behavioural change somewhere far away, and so aren't satisfactory
>> either. So types must always be specified if they are to be used, or
>> any inference that is utterly essential must be very narrowly
>> circumscribed.
>
> I agree that inference must be narrowly circumscribed and we should only do very local inference.  An interesting question is what type annotations should be silently inferred (e.g., "for" method) and which must be explicitly inserted (perhaps with the help of an inferencer).
One way around the inference problems is to say that the IDE does
that, and puts them into the source code explicitly (like the tool
Kim's student is building). Then there is no problem with the dynamic
semantics, but there is probably still more work for the programmer.
-Michael