Numbers

In LIGO, there are two types of numbers: integers and natural numbers.

• Integer literals are the same found in mainstream programming languages, for example, 10, -6 and 0, but there is only one canonical zero: 0 (so, for instance, -0 and 00 are invalid).

Contrary to integral numbers in other programming languages, numbers in LIGO have arbitrary-precision, that is, they do not overflow or underflow.

Digits of large numbers can be separated by an underscore, to increase readability.

// The following are integers

const zero = 0

const million = 1_000_000 // Grouping in French

const baekman = 100_0000 // Grouping in Korean

// The following are natural numbers

const zero_nat = 0n

const million_nat = 1_000_000n

const baekman_nat = 100_0000n

As a form of documentation, a type can be ascribed to each constant:

const zero : int = 0

const million : int = 1_000_000

const baekman : int = 100_0000

const zero_nat : nat = 0 as nat

const million_nat : nat = 1_000_000 as nat

const baekman_nat : nat = 100_0000 as nat

Casting

In mathematics, natural numbers are a strict subset of integers, and can be used in any context where an integer is expected. In LIGO, this property does not hold true in general. Instead, a given binary arithmetic operation, say, is defined four times, so it can apply to any combination of natural numbers and integers: this is called overloading, and some programming languages extend it to user-defined functions (e.g. members in C++) -- but not LIGO.

So there are no implicit type casts in LIGO, but we can explicitly cast natural numbers to integers (this is safe in all contexts where an integer is valid) by calling the predefined function int. The inverse cast, from int to nat is called in mathematics the absolute value, or abs in LIGO.

const one : int = int(1 as nat); // Explicit cast from nat to int

const two : nat = abs(2); // Explicit cast from int to nat

Adding

Addition in LIGO is accomplished by means of the + binary operator, which is overloaded to apply to any combination of natural numbers and integers, as shown in the following examples. Note that adding an integer to a natural number produces an integer, because the compiler cannot determine, in general, whether the result would be always a natural number for all inputs.

const a : int = 5 + 10; // int + int yields int

const b : nat = (5 as nat) + (10 as nat); // nat + nat yields nat

const c : int = (5 as nat) + 10; // nat + int yields int

const d : int = 10 + (5 as nat); // int + nat yields int

// const error : nat = (5 as nat) + 10;

Subtracting

Subtraction in LIGO is accomplished by means of the - binary operator which is overloaded to apply to any combination of natural numbers and integers, as shown in the following examples. The rule when subtracting two natural numbers is that the result is an integer because, in general, the compiler cannot determine whether the value of an expression is positive or zero for all inputs.

const a : int = 5 - 10; // int - int yields int

const b : int = (5 as nat) - (2 as nat); // nat - nat yields int

const c : int = (10 as nat) - 5; // nat - int yields int

const d : int = 5 - (10 as nat); // int - nat yields int

// const error : nat = (5 as nat) - (2 as nat);

Negating

The arithmetic negation of a number is the same as subtracting that number from zero, so the negation of a natural numbers yields an integer:

const a : int = -5; // - int yields int

const b : int = -(5 as nat); // - nat yields int

// const error : nat = -(5 as nat);

Multiplying

Multiplication in LIGO is accomplished by means of the * binary operator which is overloaded to apply to any combination of natural numbers and integers, as shown in the following examples. The type rules for multiplication are the same as for the addition:

const a : int = 5 * 10; // int * int yields int

const b : nat = (5 as nat) * (2 as nat); // nat * nat yields nat

const c : int = (10 as nat) * 5; // nat * int yields int

const d : int = 5 * (10 as nat); // int * nat yields int

Dividing

Because LIGO features neither floating-point nor fixed-point arithmetic, division in LIGO is Euclidean. The predefined binary operator / returns the quotient and is overloaded like the multiplication. Of course, division by zero triggers an exception that interrups the execution, so the programmer must make sure this case cannot happen because the compiler cannot determine, in general, if a variable will have a given value (or not) for all inputs.

const a : int = 10 / 3; // int / int yields int

const b : nat = (10 as nat) / (3 as nat); // nat / nat yields nat

const c : int = (10 as nat) / 3; // nat / int yields int

const d : int = 10 / (3 as nat); // int / nat yields int

The binary operator % returns the positive modulo of the Euclidean division, that is, the following holds:

(n*(a/n)+(a%n) == a) && ((0 as nat) <= a % n) && (a % n < abs(n))

It is overloaded as the Euclidean division / to allow for all four combinations of natural numbers and integers.

const a : nat = 120 % 9; // int % int yields nat

const b : nat = (120 as nat) % 9; // nat % int yields nat

const c : nat = (120 as nat) % (9 as nat); // nat % nat yields nat

const d : nat = 120 % (9 as nat); // int % nat yields nat

For cases when you need both the quotient and the remainder, LIGO provides the ediv operation. ediv(x,y) returns Some (quotient, remainder), unless y is zero, in which case it returns None. The function ediv is overloaded to accept all the combinations (4) of natural and integer numbers:

// All below equal Some (7,2)

const ediv1: option<[int, nat]> = ediv(37, 5);

const ediv2: option<[int, nat]> = ediv(37 as nat, 5);

const ediv3: option<[nat, nat]> = ediv(37 as nat, 5 as nat);

const ediv4: option<[int, nat]> = ediv(37, 5 as nat);

The ediv operation returns an option type which is Some if the result is defined and None if it is not, as when you try to divide by zero. To handle option types, see Matching.

Checking positivity

You can check if a value is a natural number (nat) by using a predefined cast function which accepts an integer (int) and returns an optional natural number (nat): if the result is None, then the given integer was positive, otherwise the corresponding natural number n is given with Some(n).

const one_is_nat: option<nat> = is_nat(1);

Increment and decrement operators

The increment operator (++) adds one to a number, and the decrement operator (--) subtracts one from a number.

You can use these operators as independent statements, as in these examples:

const testIncDecIndependent = (() => {

let value = 0;

value++;

Assert.assert(value == 1);

value--;

Assert.assert(value == 0);

})();

You can also use these operators in expressions that do other things. The order of operations for the expressions depends on whether the operator is before or after the value:

• In the prefix position (++p) the operator increments the value and returns the updated value for use in the current expression.

• In the postfix position (p++) the operator increments the value but returns the old value before the increment for use in the current expression.

const testIncEmbedded = (() => {

let value = 0;

// Prefix increment operator adds one immediately

Assert.assert(++value == 1);

Assert.assert(value == 1);

// Postfix increment operator adds one after the expression is evaluated

Assert.assert(value++ == 1);

Assert.assert(value == 2);

})();