[Grace-core] On Gradual Typing

[Lex Spoon]

>> 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.
>
> I had assumed that the point of a type-checker was to help me find errors,
> not to stop me writing an abstract superclass.

That seems like a killer observation.

I'm not sure, but it might help to make abstractness be gradual. It's
fun to say anyway. :) The idea would be that if a class is marked
neither "abstract" nor "concrete", then the compiler should assume the
class might be abstract and further that it might have abstract
members that the programmer has not specified. In the strict mode of
the compiler, all classes would need to be marked as either abstract
or concrete; gradually concrete would no longer be allowed.

For the larger story Michael has raised about gradual type checking, I
find it easier to think about literals, because literals normally
don't require a type annotation. Here's a simple example:

    print(3 + 4 - "not a number")

The story about how gradual typers leave out error messages is that
the programmer leaves out type annotations in parts of the program
that they don't want type checking to happen. In this code, there are
no types to leave out, because even in the strictest type-checking
mode, the code has no type annotations. As such, this code must do the
same thing in gradual mode and strict mode. Presuming the code has an
error in strict mode, that means it must have an error in gradual mode
as well.

That might well be considered fine. Unlike with the possibly abstract
class example, this code really is a definite error.

Lex