Notation¶
This section introduces some of the notation we use in this document and in our Agda formalization.
Propositions, Sets and Types¶
See Sets & Maps.
Note that Agda denotes the primitive notion of type by Set. To
avoid confusion, throughout this document and in our Agda code we call this primitive
Type and use ℙ for our set type.
Lists¶
We use the notation
a ∷ as for
the list with head
a and tail as;
[] denotes the empty list, and
l ∷ʳ x appends the element
x to the end of the list l.
Sums and Products¶
The sum (or disjoint union, coproduct, etc.) of A and
B is denoted by
A ⊎ B, and their product
is denoted by A × B. The
projection functions from products are denoted proj₁ and
proj₂ and the injections are denoted
inj₁ and
inj₂, respectively. The
property of being an element of a coproduct in the left (resp., right) component is called
isInj₁ (resp., isInj₂).
Addition of Map Values¶
The expression
∑[
x
←
m
]
f
x
denotes the sum of the values obtained by applying the function
f
to the values of the map
m.
Record types¶
These are explained in Agda Essentials.
Postfix Projections¶
Projections can be written using postfix notation. For example, we may
write
x
.
proj₁
instead of
proj₁
x
Restriction, Corestriction and Complements¶
The restriction of a function or map
f
to some domain
A
is denoted by
f
|
A,
and the restriction to the complement of A is written
f
|
A
ᶜ.
Corestriction or range restriction is
denoted similarly, except that | is replaced by
∣^.
Inverse Image¶
The expression m ⁻¹ B denotes the
inverse image of the set B under the map m.
Left-biased Union¶
For maps m and m', we write
m ∪ˡ m' for their left-biased union.
This means that key-value pairs in m are guaranteed to be in the union,
while a key-value pair in m' is in the union if and only if the key is
not in m.
Map Addition¶
For maps m and m', we write
m ∪⁺ m' for their union, where keys
that appear in both maps have their corresponding values added.
Mapping a Partial Function.¶
A partial function is a function on A which may not be defined for
all elements of A. We denote such a function by
f : A ⇀ B.
If we happen to know that the function is total (defined for all elements of
A), then we write f : A → B.
The mapPartial operation takes such a function
f and a set
S of elements of
A and applies
f to the elements of
S at which it is defined; the result is the set
{ f x ∣ x ∈ S and f is defined at x.}
The Maybe Type¶
This type represents an optional value and can either be
just x (indicating the presence of a value,
x) or nothing (indicating the absence of a value).
If x has type X, then
just x has type
Maybe X.
The symbol ~ denotes (pseudo)equality of two values
x and y of type
Maybe X : if x is of the form
just x' and y is
of the form just y', then
x' and y' have to be equal. Otherwise, they are
considered "equal."
The Unit Type¶
⊤ has a single inhabitant
tt and may be thought
of as a type that carries no information; it is useful for signifying the
completion of an action, the presence of a trivial value, a trivially
satisfied requirement, etc.
Superscripts and Other Special Notations¶
In the current version of this specification, superscript letters are sometimes used for things such as disambiguations or type conversions. These are essentially meaningless, only present for technical reasons and can safely be ignored. However there are the two exceptions:
-
∪ˡfor left-biased union -
ᶜin the context of set restrictions, where it indicates the complement
Also, non-letter superscripts do carry meaning.
(At some point in the future we hope to be able to remove all those non-essential superscripts. Since we prefer doing this by changing the Agda source code instead of via hiding them in this document, this is a non-trivial problem that will take some time to address.)