Functions

A function is defined by an operator of sort
domain:⇅(𝕊) → image:𝕊

Function application is denoted by square brackets:
((domain:𝕊) → (image:𝕊))[domain] : image

Functions can be composed:
(intermediate:𝕊 → image:𝕊) ⚬ (domain:𝕊 → intermediate:𝕊) : (domain:𝕊 → image:𝕊)

The application of a composed function is defined by:
domain_:𝕊, intermediate_:𝕊, image_:𝕊, f:(intermediate_ → image_), g:(domain_ → intermediate_), x:domain_, (f ⚬ g)[x] ⇒ f[g[x]]

Example

Uses _realFunction Real numbers

The function
_realFunction square : ℝ → ℝ.nn
computes the square of its argument:
_realFunction square[x:ℝ] ⇒ x × x

Application:
_realFunction square[2/3] ⇒ 4/9

Application of the squaring function composed with itself:
_realFunction (square ⚬ square)[2/3] ⇒ 16/81

Functions vs. operators

The squaring function could have equally well be defined as an operator:
_realFunction square(ℝ) : ℝ
_realFunction square(x:ℝ) ⇒ x × x

Either choice has advantages and disadvantages.

The advantage of the operator is that it can be specialized for subsorts. For example, we could add
_realFunction square(ℤ) : ℕ

The advantage of the function is that it is a term on its own that can be used without arguments. See for example the definition of the derivative in Derivatives of real functions of one variable.

Contravariance of the domain sort

In the sort declaration
domain:⇅(𝕊) → image:𝕊,
the domain sort parameter is marked as contravariant , which means that in subsort tests, its sort hierarchy is inverted. This is best illustrated by an example, which uses _{contravariance} Real numbers.

Consider an operator _{contravariance} applyToOneThird(ℚ → ℚ) : ℚ, which takes as argument a function from rational number to rational numbers and applies this function to the number _{contravariance} 1/3. The corresponding rule is:
_{contravariance} applyToOneThird(f:(ℚ → ℚ)) ⇒ f[1/3]

Can we apply this operator to a function from integers to integers? Let's try:
_{contravariance} f1 : ℤ → ℤ
_{contravariance} applyToOneThird(f1) : [ℝ]

The resulting term does not have a proper sort, so something went wrong. Let's try something else: a function from real numbers to integers:
_{contravariance} f2 : ℝ → ℤ
_{contravariance} applyToOneThird(f2) : ℚ

This yields a proper term with a proper sort. A function from real numbers to integers is indeed also a function from rational numbers to rational numbers: it accepts any rational number as its argument (plus more, but we don't care about this), and it produces a rational number (more precisely, an integer, but we don't care about this precision).