[Grace-core] On Gradual Typing

[James Noble]

"I'm not sure, but it might help to make abstractness be gradual."

This is a good principle I can't remember being elucidated before.  Not just abstract  but a bunch of other principles too... Valueness, constness, a bunch of other stuff. Having extensible annotations is part of this but there will no doubt be more...

I like abstract as an annotation, but that means e.g. Abstract methods or classes still need bodies, if abstract is in a level above the core language 

J

-----Original Message-----
From: "Lex Spoon" <lex at lexspoon.org>
Sent: ‎19/‎07/‎2013 14:08
To: "Andrew P Black" <andrew.p.black at gmail.com>
Cc: "grace-core at cecs.pdx.edu" <grace-core at cecs.pdx.edu>
Subject: Re: [Grace-core] On Gradual Typing

>> 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
_______________________________________________
Grace-core mailing list
Grace-core at cecs.pdx.edu
https://mailhost.cecs.pdx.edu/mailman/listinfo/grace-core
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mailhost.cecs.pdx.edu/pipermail/grace-core/attachments/20130719/68d45222/attachment.html>