Idea: replace attributes with arbitrary expressions

[robin-aws]

Summary

Replace the current unchecked attribute syntax with arbitrary expressions, most often datatype values.

Background and Motivation

A common pain point is mis-spelling an attribute name and having the intended effect silently fail. For example adding {:tailrecursive} instead of {:tailrecursion} on a function or method has no effect and raises no errors.

Attributes are also not as self-documenting as other elements that can be referenced in a Dafny program: if you see a call to FooBar(42), you can hover over it to see its declaration, or select "Go To Definition" to inspect it in detail. There is no such help for attributes in any tooling to date.

Proposed Feature

Instead of the current {:<name>, <argument>*} syntax, we would add syntax for attaching an arbitrary expression as metadata to the same places within the AST. By requiring that these expressions resolve and type check successfully, we ensure that typos and other misuse results in errors. This appears to be a very nice solution for Dafny specifically because it already has an extremely rich sub-language for side-effect free expressions, and static evaluation of fairly sophisticated expressions is highly feasible and already present to a degree in the pipeline.

As a straw-person argument I'd suggest following the lead of C#, Java, Python, and other languages and using @. For example:

// --- (In a prelude of some kind:) ---

// Meta-attributes

datatype AttributeTarget = Method | Function | Newtype | ...
datatype Attribute = Attribute(targets: set<AttributeTarget>, ...)

// Requires the target to be tail recursive
@Attribute(targets := {Method, Function})
datatype TailRecursion = TailRecursion

// --- (In user Dafny code) ---

@TailRecursion
function ThisBetterBeFast(x: nat): nat {
  if x == 0 then 0 else SomeOtherFunc(ThisBetterBeFast(x - 1)) // Error: not tail recursive
}

@TailRecursive // Error: TailRecursive not found
function ThisBetterBeFastToo(x: nat): nat {
  if x == 0 then 0 else SomeOtherFunc(ThisBetterBeFastToo(x - 1))
}

@TailRecursion // Error: The TailRecursion attribute cannot be applied to subset type declarations
type SmallInt = x: nat | x < 10

(I fully admit supporting arbitrary expressions rather than only datatype values may be too much power and complexity, but I'd like to start from this clean and general solution and be argued back to something more restrictive if necessary. It's likely that the general constant folding necessary for this feature could support arbitrary expressions, but that there are no solid use cases for it.)

Alternatives

We can address some of the requirements by an alternate mechanisms for registering supported attributes, their documentation, their valid use and argument types, and so on. We would also want plugins to participate in this mechanism.

[robin-aws]

@MikaelMayer also suggested using opaque predicates to solve the same problems. Perhaps that's a good reason to support arbitrary expressions as I've suggested, as uninterpreted calls to opaque predicates might end up having benefits over datatype values (although I haven't thought deeply enough to see them yet)

[atomb]

Regardless of exactly what expressions we support in the end, having the parser accept arbitrary expressions and having the type checker sort out which ones are allowed seems like a good design approach.

[MikaelMayer]

I love that proposal, especially the meta-attribute :-) I think this will be a huge leap forward. It would also enable us to rethink about annotations, for the same way we rethought about the new CLI over the previous one.
I think we will progressively replace old unchecked attributes by this new syntax. The good thing is that "@xxxx" is not yet parsed so there is no ambiguity.

I would be thrilled to see, for example down the road.

assert @Error("Unexpected unitary x") x != 1

assert @AssumeOthers X by {
  // Let's focus on this proof
}

I don't think datatypes or opaque predicates would make a difference, except if we enable pre-computing annotations, then datatypes would rock. For example, could we consider this:

function method ErrorAbout(name: string): string {
  Error("Unexpected unitary " + name)
}

const nameOfX := "first coordinate X";
method Test(x: int)
  requires @ErrorAbout(nameOfX) x != 1
}
method Main() {
  Test(1); // Error: Unexpected unitary first coordinate X
}

[robin-aws]

Regardless of exactly what expressions we support in the end, having the parser accept arbitrary expressions and having the type checker sort out which ones are allowed seems like a good design approach.

A nice side-effect of being able to implement traits with datatypes now (with --type-system-refresh and --general-traits:Datatype) is that we can define a common Attribute trait for this. It doesn't even have to be special or built-in to the language: the type checker can just ensure there is some common supertype for all annotations on a particular declaration, just as it would for a set display like {TailRecursion, Extern}.