[Grace-core] On Gradual Typing

[James Noble]

The catch with that is the core language needs to support deferred. This is partly syntactic - any empty method body still nerds to be in brackets {}.  If we went to layout syntax an empty body would just be empty.  

But the point that - if we want to have abstract layered on top of the core, then abstract annotations can't change the syntax or semantics of correct programs. But they can of course change what is thought if as correct. The same is true if any annotation. The bet we're making is that the language will be simpler and more understandable that way

J 

-----Original Message-----
From: "Kim Bruce" <kim at cs.pomona.edu>
Sent: ‎19/‎07/‎2013 19:26
To: "James Noble" <kjx at ecs.vuw.ac.nz>
Cc: "Lex Spoon" <lex at lexspoon.org>; "Andrew P Black" <andrew.p.black at gmail.com>; "grace-core at cecs.pdx.edu" <grace-core at cecs.pdx.edu>
Subject: Re: [Grace-core] On Gradual Typing

I'd like to be able to annotate methods and classes as abstract without requiring bodies.  It's a very useful style in OO programming.


Perhaps the body could just be the constant "deferred" which could have any type but blow up when touched at run time.  A static checker could consider it an error to construct an object with "deferred" appearing in it.  We'd have to explore the ramifications, but it might be a reasonable compromise.



Kim






On Jul 19, 2013, at 10:49 AM, James Noble <kjx at ecs.vuw.ac.nz> wrote:


"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


From: Lex Spoon
Sent: ‎19/‎07/‎2013 14:08
To: Andrew P Black
Cc: 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

_______________________________________________
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/20130720/1a95721a/attachment.html>