[Grace-core] On Gradual Typing

[Michael Homer]

On Fri, Jul 19, 2013 at 10:55 AM, Kim Bruce <kim at cs.pomona.edu> wrote:
> On Jul 18, 2013, at 3:21 PM, Michael Homer <mwh at ecs.vuw.ac.nz> wrote:
>> 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!).
It must be possible to call into statically-typed code from
dynamically-typed code, so it must be possible to omit the parameters.
This is especially true if you have inference; otherwise in order to
write dynamically-typed code you must write static types, and in order
to write statically-typed code you don't.

When you make such a dynamically-typed call and omit the parameters,
something must exist at runtime and the only sensible thing to
populate them with in that case is Dynamic. Exactly what the method
does with its generics you can't tell from the outside, but Dynamic is
always a valid value.

You could stipulate that generic methods can only be called with <>,
and have a different "name" to enforce this. Interaction between
dynamic and static code will then be impaired, but the generic
parameters will always be populated explicitly. Generics are likely to
creep into a lot of statically-typed public interfaces, including the
standard library - are there different collection implementations for
dynamic and static users?
-Michael