[Grace-core] On Gradual Typing

[Andrew P Black]

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

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.

> Tim has been talking about implementing the
> typechecker as a dialect for research purposes; I think that this is
> in fact the only way forward, in which the typechecker is an
> additional layer that may be bolted on for programs desiring static
> typing.

Given what you have down with the dialect mechanism, implementing a type cheater as a "checker" would seem like a great way forward. 
> 
> 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?

	Andrew