[Grace-core] On Gradual Typing

[Kim Bruce]

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/20130719/f90012a9/attachment-0001.html>