[Grace-core] On Gradual Typing

[Kim Bruce]

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

> 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

I think I would be comfortable with having the dynamically-typed code always populating omitted generics with Dynamic.  We would have to see how that works in practice, however.

This I believe is relatively new ground.  I don't know another dynamically-typed language that supports type parameters.  It would seem a bit weird to write dynamically typed code with type parameters.  This may mean that in some circumstances we might want parallel libraries for static and dynamic using code.  I'm not sure how to get around that unless we do something like Java, which results in totally broken semantics.  I'd be much happier with parallel libraries than that.