[package] [Java implementation] [Execution output]


Arithmetic


import church.lang.operators.Relational;
import church.lang.operators.Streams;
import church.lang.Error;

// Value bounds

/**
 * If defined, min_value is a per-type constant satisfying, min_value <= x, for all x of type T.
 */
abstract <T> T: min_value;

/**
 * If defined, max_value is a per-type constant satisfying, max_value >= x, for all x of type T.
 */
abstract <T> T: max_value;

// --- Ring ---

/**
 * If defined, additive_identity is a per-type constant satisfying, x + additive_identity = x, for all x of type T.
 */
abstract <T> T: additive_identity;

// Addition
abstract <T> T: (T: a) + (T: b);
// abstract <T, U>  T: (T: a) + (U: b);

// Negation (formation of the additive inverse)
abstract <T> T: -(T: a);

// Subtraction
a - b = a + (-b); // default implementation

abstract <T> T: sign(T: a);

/**
 * If defined, multiplicative_identity is a per-type constant satisfying, x * additive_identity = x, for all x of type T.
 */
abstract <T> T: multiplicative_identity;

// Multiplication
//abstract <T> T: (T: a) * (T: b);
abstract <S, T>  T: (S: a) * (T: b);

// Exponentiation. Return: a ^ b, which we define to return a value of the same type as a.
abstract <T, U> T: (T: a) ^ (U: b)

// --- Field ---

// Reciprocal (multiplicative inverse)
abstract <T> T: /(T: a);

// Division
a / b = a * (/b); // default implementation

// --- Euclidean domain ---

// A generic division interface, providing both the quotient and remainder to a supplied function.
abstract <T, U> U: divide(T: n, T: d, (T: q) −> (T: r) −> U);

// Quotient
quotient n d = divide(n, d, q −> r −> q);

// Remainder
n % d = divide(n, d, q −> r −> r);

// Divide-or-fail
n /! d = divide(n, d, q −> r −> if r != additive_identity
                                    then error("Division failed unexpectedly. "/* for " + $0 + " by " + $1*/)
                                    else q);

// Provide the Euclidean algorithm as a generic default for gcd.
gcd a b = {output << "gcd> a: " << a << ", b: " << b << "\n"; if b == additive_identity then a else gcd(b, a % b)};