2.1.12 Annotations

‹ann›: ‹name-ann› | ‹dot-ann› | ‹app-ann› | ‹arrow-ann› | ‹pred-ann› | ‹tuple-ann› | ‹record-ann›

Annotations in Pyret express intended types values will have at runtime. They appear next to identifiers anywhere a binding is specified in the grammar, and if an annotation is present adjacent to an identifier, the program is compiled to raise an error if the value bound to that identifier would behave in a way that violates the annotation. The annotation provides a guarantee that either the value will behave in a particular way, or the program will raise an exception. In addition, annotations can be checked by Pyret’s type checker to ensure that all values have the expected types and are used correctly.

2.1.12.1 Name Annotations

Any

Number

String

Boolean

Each of these names represents a particular type of runtime value, and using them in annotation position will check each time the identifier is bound that the value is of the right type.

x :: Number = "not-a-number"
# Error: expected Number and got "not-a-number"

Any is an annotation that allows any value to be used. It’s semantically equivalent to not putting an annotation on an identifier, but it allows a program to clearly signal that no restrictions are intended for the identifier it annotates.

import equality as EQ
eq-reqult :: EQ.EqualityResult = equal-always3(5, 6)

2.1.12.2 Parametric Annotations

‹app-ann›: ‹name-ann› < ‹comma-anns› > | ‹dot-ann› < ‹comma-anns› > ‹comma-anns›: ‹ann› (, ‹ann›)*

list-of-nums :: List = [list: 1, 2, 3]

list-of-nums :: List<Number> = [list: 1, 2, 3]

Note that this annotation will not dynamically check that every item in the list is in fact a Number — that would be infeasibly expensive. However, the static type checker will make use of this information more fully.

2.1.12.3 Arrow Annotations

An arrow annotation is used to describe the behavior of functions. It consists of a list of comma-separated argument types followed by an ASCII arrow and return type. Optionally, the annotation can specify argument names as well:

‹arrow-ann›: ( (‹ann› ,)* ‹ann› -> ‹ann› ) | ( ( (NAME :: ‹ann› ,)* NAME :: ‹ann› ) -> ‹ann› )

When an arrow annotation appears in a binding, that binding position simply checks that the value is a function. To enforce a more detailed check, use Contracts.

2.1.12.4 Predicate Annotations

A predicate annotation is used to refine the annotations describing the a value.

‹pred-ann›: ‹ann› % ( NAME )

For example, a function might only work on non-empty lists. We might write this as

fun do-something-with<a>(non-empty-list :: List<a>%(is-link)) -> a: ... end

If we want to write customized predicates, we can easily do so. Those predicates must be defined before being used in an annotation position, and must be refered to by name.

2.1.12.5 Tuple Annotations

Annotating a tuple is syntactically very similar to writing a tuple value:

‹tuple-ann›: { ‹ann› (; ‹ann›)* [;] }

Each component is itself an annotation.

num-bool :: {Number; Boolean} = {3; true}
num-bool--string-list :: {{Number; Boolean}; {String; List<Any>}} = {{3; true}; {"hi"; empty}}

2.1.12.6 Record Annotations

Annotating a record is syntactically very similar to writing a record value, but where the single-colon separators between field names and their values have been replaced with the double-colon of all annotations:

‹record-ann›: { ‹ann-field› (, ‹ann-field›)* } ‹ann-field›: NAME :: ‹ann›

my-obj :: {n :: Number, s :: String, b :: Boolean} = {s: "Hello", b: true, n: 42}