On this page:
:  :
:  :
Any
Any.of
Any.to_  boolean
None
:  ~
:  ~
is_  a
described_  as
matching
satisfying
converting
maybe
8.12

6.48 Annotations🔗ℹ

expression

expr :: annot

Checks that the value of expr satisifies annot, and returns the value if so.

> [1, 2, 3] :: List

[1, 2, 3]

binding operator

bind :: annot

Binds the same as bind, but first checks that the value to be bound satisfies annot.

If annot is a converter annotation, the conversion is applied before matching the converted value against bind. This dependency implies that the conversion in annot cannot be delayed, and must be performed as part of the matching process (before committing to the match).

> def x :: List = [1, 2, 3]

annotation

Any

 

annotation

Any.of(expr, ...)

 

annotation

Any.to_boolean

 

annotation

None

The Any annotation matches any value. An Any.of annotaton matches any value that is equal (in the sense of ==) to one of the expr results. The Any.to_boolean annotation matches any value and converts non-#false value to #true.

The None annotation matches no values, or in other words, is equivalent to Any.of(). It is useful for asserting that something never returns, such as a function that always throws.

> "hello" is_a Any

#true

> "hello" is_a Any.of("hello", "goodbye")

#true

> "hola" is_a Any.of("hello", "goodbye")

#false

> "hello" :: Any.to_boolean

#true

> #false :: Any.to_boolean

#false

> "will not match" is_a None

#false

> "will not match" is_a Any.of()

#false

expression

expr :~ annot

Associates static information to the overall expression the same as ::, but performs no run-time check on the value of expr. The annot must specify a predicate annotation.

> [1, 2, 3] :~ List

[1, 2, 3]

> "oops" :~ List

"oops"

binding operator

bind :~ annot

Associates static information to bind the same as ::, but performs no run-time check. The annot must specify a predicate annotation.

> def x :~ List = [1, 2, 3]

> def x :~ List = "oops"

expression

expr is_a annot

Produces #true if the value of expr satisfies annot, #false otherwise.

If annot is a converter annotation, only the matching component of the annotation is used, and the converting part is not used. See also Annotations as Converters.

> [1, 2, 3] is_a List

#true

> "oops" is_a List

#false

binding operator

bind described_as term ...

Equivalent to bind, but when a binding match fails in a way that triggers an error message (as opposed to moving on to a different binding pattern), the message describes the expected annotation as term .... The term ... sequence is not parsed, so it can be any sequence of terms.

> def (x :: Int) described_as An Integer = "oops"

def: value does not satisfy annotation

  value: "oops"

  annotation: An Integer

annotation

matching(bind)

Converts bind into an annotation. Variables bound in bind are not made visible, but the annotation corresponds to the set of values for which bind would match. Since no results are made visible, bind is used only in matching mode, and implied conversions might be skipped.

> def x :: matching([_, 10]) = [9, 10]

> def y :: matching([_, 10]) = [9, 11]

def: value does not satisfy annotation

  value: [9, 11]

  annotation: matching([_, 10])

Produces a predicate annotation using the resulting function from pred_expr.

fun is_multiple_of(n):

  fun (v):

    v is_a Int && v mod n == 0

> 15 :: (satisfying(is_multiple_of(3))

           && satisfying(is_multiple_of(5)))

15

fun

| is_list_with_one(lst :: List):

    lst.has_element(1)

| is_list_with_one(_):

    #false

> [1, 2, 3] :: satisfying(is_list_with_one)

[1, 2, 3]

> Array(1, 2, 3) :: satisfying(is_list_with_one)

::: value does not satisfy annotation

  value: Array(1, 2, 3)

  annotation: satisfying(is_list_with_one)

annotation

converting(fun (bind) maybe_res_annot:

             body

             ...)

 

maybe_res_annot

 = 

:: annot

 | 

:~ annot

 | 

ϵ

Produces a converter annotation by pairing bind with body. The annotation matches when bind matches, but the value produced by the annotation is determined by the body sequence, which can refer to variables bound by bind.

When annot is provided, then its static information is propagated to the new converter annotation. If annot is supplied with ::, then the result of the body sequence is checked against annot.

See also Annotations as Converters.

> def x :: converting(fun (x :: Int): x + 1) = 11

> def x :: converting(fun (x :: Int): x + 1) = "eleven"

def: value does not satisfy annotation

  value: "eleven"

  annotation: converting(fun (x :: Int): x + 1)

annotation

maybe(annot)

Equivalent to False || annot, which is an annotation that is satisfied by either #false or a value that satisfies annot. If annot is a converter annotation, its conversion applies to a non-#false value.

> #false :: maybe(String)

#false

> "string" :: maybe(String)

"string"

> #true :: maybe(String)

::: value does not satisfy annotation

  value: #true

  annotation: maybe(String)