On this page:
2.1.12.1 Name Annotations
2.1.12.2 Parametric Annotations
2.1.12.3 Arrow Annotations
2.1.12.4 Predicate Annotations
2.1.12.5 Tuple Annotations
2.1.12.6 Record Annotations
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

‹name-ann›: NAME ‹dot-ann›: NAME . NAME

Some annotations are simply names. For example, a data declaration binds the name of the declaration as a value suitable for use as a name annotation. There are built-in name annotations, too:

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.

Dot-annotations allow for importing types from modules:

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›)*

Many data definitions are parametric, meaning they can contain any uniform type of data, such as lists of numbers. Accordingly, while the following annotation isn’t quite wrong, it is incomplete:

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

To properly express the constraint on the contents, we need to specialize the list annotation:

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.

For example we could write

Examples:

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›

As with object literals, the order of fields does not matter. For example,

Examples:

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