Proposed Extension: "abstract declarations" (marker declarations)

I am proposing a small language extension, which I'm calling "abstract declarations", because they are declarations (they make a name visible) but have no associated definitions. Two examples to give you the idea:

method speed is required ;

def immutable is annotation ;

Note that neither of these forms is currently legal; they start off like a method or def declaration, but give no value to the method or def. (The semicolon is there to emphasise that point; a newline would work equally-well, of course.) These examples are motivated by two use cases that we need to support, but currently don't.

The first use case is required methods. Currently, minigrace supports the idea of required methods by making the programmer write

method speed { required } ;

This had the advantage that it could be accommodated without needing to change the existing minigrace parser (required is just a method that raises a runtime error), but it has the disadvantage that it's wrong. What I mean by that is that required methods are not real methods; in particular, they don't ever override a real method written by the programmer. Rather, their function is to signal (signify?) that a real method must be provided. So, when composing traits, required methods must be treated specially. It's much more reasonable to do this if there is a special syntax for them than if they are just ordinary methods whose bodies take a specific form.

For example, if I define

method explicitRequirement { required }

and write in a trait

method position { explicitRequirement }

then is position a required method or a normal method?

We could also use abstract declarations for abstract methods

method acceleration is abstract

which would make it more natural to treat abstract methods specially (in a dialect or in the base language), to, for example, prevent instantiation of abstract classes.

The second use case for abstract declarations is defining annotations themselves. My first thought was to treat annotations as values, and to declare new ones by writing something like

def private = annotation

where annotation would be an object factory that generates a new unique annotation. But this seems like a bad idea; for example, a student might write

def private = public

which would presumably make private and public mean the same thing! Interpreting these annotations would required that the compiler does data-flow, and that we have more manifest rules to make this possible.

This line of thought led me to the position that annotations should be identifiers, i.e., compile-time labels, not runtime values. A def declaration is public because the word public is attached to it, not because it is annotated with an expression that somehow can be proved to evaluated to public. This is what Java's @annotation syntax does; if the purpose of the annotation is to include information for the programmer or the compiler, then it seems most reasonable to make annotations static labels rather than dynamic values. (This does't stop a reflection system from asking about those labels at runtime; this is what Java's @retained is about. I suspect that all Grace annotations should be retained, since the only reason not to retain them would be efficiency, which we don't care about.)

This leaves us with the question off how to declare new annotations. One option is not to declare them at all; they would be implicitly declared by virtue of their appearing after an is. This seems error-prone and inconsistent with the rest of Grace. We could have a new declarative form:

annotation private

but that seems rather heavyweight.

So I'm suggesting that we use an abstraction over existing declarative forms

def private is annotation
method author(name) is annotation

which could be used to declare annotations without and with arguments. We could even (I think) use type arguments

method owned⟦O⟧ is annotation

but this would probably required brands to create a universe of values for O to range over. Let's not go there right now.

One thing I'm not all that happy about: the term "abstract declaration". This might make some people think that they have to do with abstract classes or methods. Pascal (and C) call declarations without bodies "forward declarations" but uses them for a slightly different purpose. How about:

empty declaration
maker declaration
vacuous declaration

This hasn't sparked a lot of objections, so I started implementing it — I need to do something about annotations in SmallGrace.

One of the great things about having a parser generator that works from a grammar is that it will complain if the grammar is ambiguous. It turns out that the general case where an annotation is an arbitrary request is ambiguous. The tricky case is where the annotation is a method that is given a literal block as its argument. Then, you can't tell whether

method example is marsupial { pouch(kanga) }

is a method with annotation marsupial and body pouch(kanga), or a method with annotation marsupial(_) with argument pouch(kanga) and no method body. (Even if the method body were always required, disambiguating these cases would require unbounded lookahead, so they would still be beyond what a parser-generator with one symbol lookahead, or a human, would accept.)

Since we don't yet have any use cases for annotations with parameters, let alone annotations with blocks as parameters, I plan to disambiguate these cases by requiring parentheses around an annotation argument that is a block. Hence, the above example will be interpreted as a method with body pouch(kanga). If one wants the block to be an argument to the annotation, one would have to write

method example is marsupial({ pouch(kanga) }) {
    body
}

I don't particularly like this, but it is a case that is unlikely to arise in practice, so the ugliness of the multiple brackets probably won't worry anyone.

I'm tending towards calling them "marker declarations"

Ugly, but I don’t have better ideas at the moment.

Kim

On Mar 5, 2018, at 2:47 PM, Andrew Black notifications@github.com wrote:

This hasn't sparked a lot of objections, so I started implementing it — I need to do something about annotations in SmallGrace.

One of the great things about having a parser generator that works from a grammar is that it will complain if the grammar is ambiguous. It turns out that the general case where an annotation is an arbitrary request is ambiguous. The tricky case is where the annotation is a method that is given a literal block as its argument. Then, you can't tell whether

method example is marsupial { pouch(kanga) } is a method with annotation marsupial and body pouch(kanga), or a method with annotation marsupial(_) with argument pouch(kanga) and no method body. (Even if the method body were always required, disambiguating these cases would require unbounded lookahead, so they would still be beyond what a parser-generator with one symbol lookahead, or a human, would accept.)

Since we don't yet have any use cases for annotations with parameters, let alone annotations with blocks as parameters, I plan to disambiguate these cases by requiring parentheses around an annotation argument that is a block. Hence, the above example will be interpreted as a method with body pouch(kanga). If one wants the block to be an argument to the annotation, one would have to write

method example is marsupial({ pouch(kanga) }) { body } I don't particularly like this, but it is a case that is unlikely to arise in practice, so the ugliness of the multiple brackets probably won't worry anyone.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/gracelang/language/issues/162#issuecomment-370595492, or mute the thread https://github.com/notifications/unsubscribe-auth/ABuh-qV9rAZ1OnHcNp-imS0sEweVeS3Uks5tbcCKgaJpZM4SZTln.

Ugly, but I don’t have better ideas at the moment.

not put anything straight into the spec then?

The tricky case is where the annotation is a method that is given a literal block as its argument. Then, you can't tell whether

Since we don't yet have any use cases for annotations with parameters, let alone annotations with blocks as parameters,

method foo(x,y) is requires { x > 0, y > 0 } ensures { rv -> ((rv % x) == 0) && ((rv % y) == 0) }

oops.

if we write

def x is public = 4 type newtype[[T,O]] is owned(O) = interface { .. }

and should write

var v is confidential = 5

perhaps we have to complete the square:

method m(x, y) -> 6 is public = { ... } class m(x, y) -> 6 is public = { ... }

not that I like that either but yet one character to O'CAML

I sort of like the idea of using = in method definitions. We might take it all the way and write, rather than

method m(x, y) -> 6 is public = {  ... }

something like

def m:6 is public = {x, y → 6}

where the arguments are pushed to the rhs of the =. Haskel allows this for function definitions, (and ML too?) but it's not normally used, for the good reason that it's harder to read than the notation that we have.

Using = in this way also has the disadvantage that it's lying to the reader. A method is not block; the problem is not self, but return. Methods bind return; blocks do not. So we would have to write:

def m:6 is public = method {x, y → 6}

Quite apart from the questionable legality of using 6 as a type, this seems worse than the problem that we are trying to solve.

A respect for basic English leads me to:

method foo(x,y) is sepecifiedBy [
    requires { x > 0,  y > 0 }, 
    ensures { rv → ((rv % x) == 0) && ((rv % y) == 0) }
] { return x * y }

But this example shows that we have a lot more problems than just syntax! In the examples of invariants and conditions that Michael got running in a dialect, the predicates were in the method body, and were executed. If we put them in an annotation, then they are not going to be executed; presumably the intention is that the dialect prove them correct. But that means that the dialect doesn't want blocks: it wants source code. I suppose that it could get the source code back from the AST of the method, but if the conditions are not going to be executed, the dialect may as well get strings.

This might be a good project for a PhD. It seems that the dialect might want to do a combination of run-time and static checking. If we let the dialect change type annotations, it could get the post condition checking in by munging the return type to be a pattern. Pre-condition checks are tricker, because invariants that involve multiple parameters aren't expressible with Grace's type annotations, and loop variants and invariants really require more.

In short, an extra pair of parens is the least of our problems. We already require them around pattern expressions that are simple identifiers, and around arguments that are requests ...

I'm closing this issue because it is now in the spec, as well as being implemented in SmallGrace and in miningrace

gracelang / language

Proposed Extension: "abstract declarations" (marker declarations) #162