The Avail Programming Language
Mobile Users: Click here to view our text rendering warning.

extended integer ≝ [-∞..∞]

Type lattice: focus on extended integer. any any ⊤--any nontype nontype any--nontype number number nontype--number extended integer extended integer = [-∞..∞] number--extended integer -∞ type {-∞}ᵀ extended integer---∞ type integer integer = (-∞..∞) extended integer--integer ∞ type {∞}ᵀ extended integer--∞ type -∞ type--integer -∞ type--⊥ integer--∞ type nonpositive integer nonpositive integer = (-∞..0] integer--nonpositive integer whole number whole number = [0..∞) integer--whole number ∞ type--⊥ negative integer negative integer = (-∞..-1] nonpositive integer--negative integer nonpositive integer--whole number natural number natural number = [1..∞) negative integer--natural number negative integer--⊥ whole number--natural number code point code point = [0..1114111] whole number--code point byte byte = [0..255] whole number--byte natural number--code point [1..6] [1..6] natural number--[1..6] [2..11] [2..11] natural number--[2..11] [42..49] [42..49] natural number--[42..49] code point--byte byte--[1..6] byte--[2..11] byte--[42..49] …[1..6] …[1..6]--[1..6] [42..49]… …[2..5] [2..5] [2..5] …[2..5]--[2..5] [7..9]… [1..6]--⊥ [1..6]--[2..11] [1..6]--[2..5] [2..11]--[42..49] [2..11]--[2..5] [7..9] [7..9] [2..11]--[7..9] [42..49]--[42..49]… [42..49]--⊥ [2..5]--⊥ [2..5]--[7..9] [7..9]--[7..9]… {7}ᵀ {7}ᵀ [7..9]--{7}ᵀ {8}ᵀ {8}ᵀ [7..9]--{8}ᵀ {9}ᵀ {9}ᵀ [7..9]--{9}ᵀ {7}ᵀ--⊥ {7}ᵀ--{8}ᵀ {8}ᵀ--⊥ {8}ᵀ--{9}ᵀ {9}ᵀ--⊥

An integer is a discrete number, i.e., it has no fractional part. As such, integers are excellent for counting and labeling.

The literal representation of an integer is a sequence of one or more decimal digits, such as 0, 1, 200, 50000, or 598798234908600912387587829348623580980827481650893468592374832569783. Negative integer literals are created using the method "-_", which defines a semantic restriction that strengthens the answer's type to an instance type whenever the argument's value is precisely known, as is the case for -1 or -42. and -∞ are positive and negative infinity, respectively.

Avail's integral type specifies four parameters for completion:

  • The lower bound is an integer which specifies the smallest allowed value. The floor operation, "⎣_⎦", answers the lower bound of an integral type.
  • The lower bound inclusion indicator is a boolean value that establishes whether the lower bound is a member of the integral type. When this value is true, then the lower bound is included in the type's membership. When this value is false, then it is not so included. The method "⎣_⎦is inclusive" answers the lower bound inclusion indicator of an integral type.
  • The upper bound is an integer which specifies the largest allowed value. The ceiling operation, "⎡_⎤", answers the upper bound of an integral type.
  • The upper bound inclusion indicator is a boolean value that establishes whether the upper bound is a member of the integral type. When this value is true, then the upper bound is included in the type's membership. When this value is false, then it is not so included. The method "⎡_⎤is inclusive" answers the upper bound inclusion indicator of an integral type.

The primitive integral type constructor is "integer range from_(inclusive=_)to_(inclusive=_)". As expected from the name, it accepts the lower bound, lower bound inclusion indicator, upper bound, and upper bound inclusion indicator, respectively. This method supports the most general type construction case, that of four statically unknown type completion arguments. Most type construction is done by the compiler during execution of type annotations, however, so typically most or all of the integral type completion arguments will be known at compile-time. For these cases, the system library provides the following convenience methods:

  • The method "[_.._]" accepts two arguments, the lower and upper bounds, respectively, and constructs an integral type whose bounds are both inclusive.
    Assert: 1 ∈ [1..10]; Assert: 10 ∈ [1..10];
  • The method "[_.._)" accepts the same arguments and constructs an integral type whose lower bound is inclusive and whose upper bound is exclusive.
    Assert: 1 ∈ [1..10); Assert: 10 ∉ [1..10);
  • The method "(_.._]" accepts the same arguments and constructs an integral type whose lower bound is exclusive and whose upper bound is inclusive.
    Assert: 1 ∉ (1..10]; Assert: 10 ∈ (1..10];
  • The method "(_.._)" accepts the same arguments and constructs an integral type whose bounds are both exclusive.
    Assert: 1 ∉ (1..10); Assert: 10 ∉ (1..10);

Irrespective of which integral type constructor is chosen, a canonization step converts an exclusive bound into an equivalent inclusive bound whenever possible — that is, when the bound is not infinite.

/* Both bounds are canonized. The lower bound is adjusted upward by one, and the * lower bound inclusion indicator becomes "true". Correspondingly, the upper * bound is adjusted downward by one, and the upper bound inclusion indicator * becomes "true". */ Assert: (1..10) = [2..9]; Assert: ⎣(1..10)⎦ = 2; Assert: ⎣(1..10)⎦ is inclusive; Assert: ⎡(1..10)⎤ = 9; Assert: ⎡(1..10)⎤ is inclusive; /* Only the finite lower bound is canonized. */ Assert: (1..∞) = [2..∞); Assert: (1..∞) ≠ [2..∞]; Assert: ⎣(1..∞)⎦ = 2; Assert: ⎣(1..∞)⎦ is inclusive; Assert: ⎡(1..∞)⎤ = ∞; Assert: ¬⎡(1..∞)⎤ is inclusive; /* Only the finite upper bound is canonized. */ Assert: (-∞..1) = (-∞..0]; Assert: (-∞..1) ≠ [-∞..0]; Assert: ⎣(-∞..1)⎦ = -∞; Assert: ¬⎣(-∞..1)⎦ is inclusive; Assert: ⎡(-∞..1)⎤ = 0; Assert: ⎡(-∞..1)⎤ is inclusive;

The system library provides type names for several useful integral types. extended integer is an alias for [-∞..∞], the most general integral type; it includes all finite integers, plus negative infinity (-∞) and positive infinity (). integer is defined as (-∞..∞), and is the type of all finite integers. whole number is [0..∞), and describes all counting numbers. natural number is [1..∞), and is the type of subscripts. code point is [0..1114111] expresses the range of valid Unicode code points. byte is an unsigned 8-bit integer ([0..255]), and is primarily useful for I/O operations. On the other end of the number line are nonpositive integer(-∞..0] — and negative integer(-∞..-1].

float | Return to Type System | tuple