[Grace-core] On Gradual Typing

[Michael Homer]

On Fri, Jul 19, 2013 at 10:16 AM, Andrew P Black
<andrew.p.black at gmail.com> wrote:
>
> On 17 Jul 2013, at 02:56 , Michael Homer wrote:
>
>> Let us consider the following completely statically-typed program:
>> 1    object {
>> 2        method x -> Done {
>> 3            self.y
>> 4        }
>> 5    }
>
> Is this a complete program?  Or a fragment of a program?   If it's a complete program, we know exactly what it's semantics will be: to create an object and then discard it, without ever executing any of its methods.   As such, it is not an error — although some warnings about dead code or unresolved names might be in order.
I imagine that any reasonable typechecker will raise an error here
notwithstanding (and perhaps then complain as well that the object
goes nowhere). self has a known static type; y is not in this type;
this request is an error.
> I expect that you want it to be a program fragment.  In that case, whether it's an error depends on the context.   What does this object inherit from — perhaps that can depend on the dialect?  What's the enclosing context (not relevant here, but it would be if we had written y rather than self.y)?   What objects inherit from this one (yes, I remember that we outlawed object inheritance in Montpellier, but the above fragment may be the result of a method).   The reason for this fragment to exist may be so that a collection of objects with different implementations of y can inherit from it.
The point is that you don't know what inherits from it (statically,
probably), and so with a static typechecker it is an error. It isn't
necessarily wrong dynamically, and if the typechecker is fully
disabled by an out-of-band lever then the program should be fine.

In my last response to Kim I give an example where inheritance is in
play, but I don't think it makes any difference to what the static
checker would do locally.
> I want an IDE that will remind me that the above object requires a y method.  I don't want an IDE that will prevent me from running tests on a program that contains such an object.
Yes you do. That is why I wrote these examples.
>> 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.
>
> Why would the type-checker need to modify the behaviour of the program?  Can you give an example?
Anywhere that you infer a generic parameter. It is an actual concrete
argument to the method.
-Michael