[Grace-core] On Gradual Typing

[Kim Bruce]

I would propose that we require declaration of abstract methods in the core language.  To me it is very much like the decision to require declarations of variables.  If you want something to be recognized, it should be declared.  Otherwise you get the same problem with typos as with missing variable declarations.

Kim



On Jul 20, 2013, at 4:07 AM, James Noble <kjx at ecs.vuw.ac.nz> wrote:

> 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
> From: Kim Bruce
> Sent: ‎19/‎07/‎2013 19:26
> To: James Noble
> Cc: Lex Spoon; Andrew P Black; 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/22109eb8/attachment-0001.html>