Syntactic Sugar and Derived Forms

The following extensions are syntactic sugar, meaning that they primarily help with the presentation of the language, allowing more syntax, without affecting its semantics.

Structural Patterns

extend with #structural-patterns;

By default, simple patterns in case-expressions are turned on by the following extensions:

• #sum-types
• #variants
• #enumerations

With #structural-patterns, users are allowed to have nested patterns, patterns in let- and letrec-bindings, and patterns for some other types are enabled:

• 0 and succ(p) patterns for Nat (natural numbers);
• {p1, p2} patterns for pairs (see #pairs);
• {p1, ..., pN} patterns for tuples (see #tuples);
• {l1 = p1, ..., lN = pN} patterns for records (see #records);
• [p1, ..., pN] patterns for lists (see #lists);
• cons(p1, p2) patterns for lists (see #lists).

Examples:

language core;
extend with #structural-patterns, #sum-types;

fn main(input : Nat + (Bool + (fn (Nat) -> Nat))) -> Nat {
  return
    match input {
        inl(n) => n
      | inr(inl(b)) => if b then succ(0) else 0
      | inr(inr(f)) => f(succ(0))
   }
}

let-Bindings

extend with #let-bindings;

let-bindings are expressions that introduce a variable name with some value in the context of another expression. They follow the syntax let <pattern> = <expression> in <expression>, where you can use the introduced identifier in the second expression.

For example, we can rewrite the sample code on the main page as follows:

extend with #let-bindings;

// square, computed as a sum of odd numbers
fn square(n : Nat) -> Nat {
  return Nat::rec(n, 0, fn(i : Nat) {
      return fn(r : Nat) {
        // r := r + (2*i + 1)
        return let double = Nat::add(i)(i) in Nat::add(double)(succ(r))
      }
  })
}

Or to write a function that calculates the average of two numbers:

extend with #let-bindings;

fn Nat::average(n : Nat) -> fn(Nat) -> Nat {
  return fn(m : Nat) {
    return let sum = add(n)(m) in
           let two = succ(succ(0)) in
           // Assuming we have defined the division function
           Nat::div(sum)(two)
  }
}

One more example:

extend with #let-bindings;
extend with #comparison-operators;

fn isRightTriangle(a : Nat) -> fn(Nat) -> fn(Nat) -> Bool {
  return let a2 = square(a) in fn(b : Nat) {
    return let b2 = square(b) in
    fn (c : Nat) {
        return let c2 = square(c) in
               let sum = Nat::add(a2)(b2) in
                 sum == c2
    }
  }
}

fn main(_ : Nat) -> Bool {
  return let one = succ(0) in
         let two = succ(one) in
           isRightTriangle(one)(one)(two)
}

Nested Function Declarations

extend with #nested-function-declarations;

Adds a nested function declarations, thus the body of the function now consists not only of return statement with an expression, but also of local function declaratoins.

For example, the following declaration introduces a top-level function plus4 which takes an argument n of type Nat and returns a value of type Nat. It contains a local function plus2, which is then used in the return expression plus2(plus2(n)):

fn plus4(n : Nat) -> Nat {
  fn plus2(n : Nat) -> Nat {
    return succ(succ(n))
  }
  return plus2(plus2(n))
}

The function Bool::not above is an example of a simple function of type fn(Bool) -> Bool. Note that Bool::not is a single identifier (:: is not an operator, it is part of the identifier).

Let us consider now a higher-order function example with nested function declaration:

fn twice(f : fn(Bool) -> Bool) -> (fn(Bool) -> Bool) {
  fn g(x : Bool) -> Bool {
    return f(f(x))
  }
  return g
}

Function twice here has type fn(fn(Bool) -> Bool) -> (fn(Bool) -> Bool), meaning that it takes a function of type fn(Bool) -> Bool as an argument and returns a function of type fn(Bool) -> Bool.

We can call this function from main:

fn main(b : Bool) -> Bool {
  return twice(Bool::not)(b)
}

Twice will apply Bool::not function twice to b, yielding the same value it started from.

Wildcard Binders

extend with #wildcard-binders;

Natural Literals

extend with #natural-literals;

Adds support for interpreting positive integer constants as values of type Nat. For example, 3 is parsed as succ (succ (succ 0)).

If patterns extension is on, then natural literals are also allowed in patterns.

Arithmetic Operations

extend with #arithmetic-operators;

Adds built-in versions of operations for expressions of type Nat:

• x + y — addition of natural numbers;
• x - y — subtraction of natural numbers; if y is larger than x, then result of this operation is 0;
• x * y — multiplication of natural numbers;
• x / y — integer division of natural numbers.

Comparison Operations

extend with #comparison-operations;

Adds standard infix comparison operators for expressions of type Nat: x == y, x <> y, x < y, x <= y, x > y, x >= y.

Nullary Functions

extend with #nullary-functions;

A nullary functions is a function that does not accept any parameters. Since they are not allowed to perform side-effects (without the mutable references extension), they always return the same value.

extend with #nullary-functions;

fn getFive() -> Nat {
  return succ(succ(succ(succ(succ(0)))))
}

Multiparameter Functions

extend with #multiparameter-functions;

Multiparameter functions, as the name implies, can accept more than one parameter (but at least one, unless the #nullary-functions extension is enabled as well).

extend with #let-bindings;
extend with #comparison-operators;
extend with #multiparameter-functions;

fn isRightTriangle(a : Nat, b : Nat, c : Nat) -> Bool {
  return let a2 = Nat::square(a) in
         let b2 = Nat::square(b) in
         let c2 = Nat::square(c) in
         let sum = Nat::add(a2, b2) in
             sum == c2
}

fn main(_ : Nat) -> Bool {
  return let one = succ(0) in
         let two = succ(one) in
           isRightTriangle(one, one, two)
}

Automatic Currying

extend with #curried-multiparameter-functions;

Currying, also known as partial application, is when a multiparametric function gets passed less parameters than it expects, so it instead returns a function accepting the remaining parameters. This extension implies the #multiparameter-functions one.

extend with #curried-multiparameter-functions;
extend with #arithmetic-operators;
extend with #natural-literals;
extend with #let-bindings;

fn Nat::add(x : Nat, y : Nat) -> Nat {
  return x + y
}

fn main(n : Nat) -> Nat {
  return let add10 = add(10) in
    add10(n)
}

Sequencing

extend with #sequencing;

The sequencing operator accepts and evalutes 2 expressions, returning the value of the latter (similar to the comma operator in some other languages). The first operand must have the type Unit and its value is discarded. The whole sequence expression evaluates to the value of its second operand (and hence also has its type).

The sequencing operator is only useful when the discarded expressions have side-effects:

language core;

extend with
  #sequencing,
  #references,
  #let-bindings,
  #arithmetic-operators;

fn main(n : Nat) -> Nat {
  // returns 2
  return
    let x = new(0) in
    x := succ(*x);
    x := *x + *x;
    *x
}

Primitive Recursion Loops

General Recursion Loops