[Grace-core] On Gradual Typing

[Kim Bruce]

On Jul 18, 2013, at 3:21 PM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:

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

We haven't talked about this yet, but I would like to require a stub for abstract (not yet defined methods), which would resolve this problem.  Languages like Java and C++ require this (and probably most other OO languages).

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

If the program execution depends on a type E, then it must do so whether it is static or dynamic.  We could try to restrict programs so that this is not visible, but that seems like overkill.  We already know that we are going to get different behavior with different types when we use match.  I.e.,
method go<E>(...) { 
   match(exp)
        case{e:E -> ...}
}

Clearly you get different behavior if you write go<Number> or go<Dynamic>.  I think once you write type-dependent code, the semantics depends on the type (that, after all was presumably the purpose!).

My gut feeling (which may be revised based on experience) is that we only do type inference if there is enough explicit type info that we know exactly the intended type.  Thus in your example above, we could infer the E parameter for go as long as x was explicitly typed so we can extract E.

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