Expressions

• Integer and string literals.
  • 17 gives the literal value 17, of type U64.
  • "Hello, world!" gives a literal of type String.
• Vector literals.
  • [1, 2, 3] gives an element of type Vector U64.
  • [] gives the empty vector with type Vector T, where T will be deduced.
• Holes, denoted by _. The compiler attempts to deduce the values of these.
  • empty_vec _ - an empty vector of unknown type (to be deduced by the compiler from how this value is used).
• Lambda functions.
  • \x.add x x - a function doubling its input.
  • \x.x - the identity function. The compiler will try to deduce the argument type.
  • \T:Type.T -> T - a function taking a type and giving the type T of endomorphisms of T.
  • \.51 - a constant function with anonymous argument, always yielding 51.
  • \:U64.68 - a constant function with anonymous argument of type U64, always yielding 68.
• Blocks consisting of a series of statements followed by an expression. See the statement section for more details.
  • block { let x = 17; let y = mul x x; sub y x } gives 272, evaluating the expression sub y x after the let statements.
• Applications of functions, notated by superposition.
  • f x - apply f to x.
  • f x y - apply f x to y. This is the usual way to write multivariate functions (see: currying).
• Applications of functions notated with \\.
  • f \\ f \\ f \\ f x - syntax sugar for f (f (f (f x))).
  • f \\ g a \\ h b c \\ i d e f - syntax sugar for f (g a (h b c (i d e f))).
• Function types.
  • U64 -> U64 - the type of functions from U64 to U64
    
  • U64 -> U64 -> U64 - the type of functions from U64 to U64 -> U64.
• Dependent function types.
  • (T : Type) -> Vector T - the type of functions that, given a type T return an element of Vector T

Statements

• An axiom declaration: axiom [name] : [type_expression];
  • axiom Nat : Type; - declare, by fiat, a new type.
  • axiom zero : Nat; - declare a new element of Nat.
  • axiom succ : Nat -> Nat; - declare a new constructor for Nat accepting one argument.
  • The compiler assumes axioms are irreducible and only allows pattern matching against axioms.
• A plain declaration: declare [name] : [type_expression];
  • declare add : Nat -> Nat -> Nat; - declare a new term, taking two Nats to an output Nat.
  • The compiler asumes plain declarations will be defined by pattern matching.
• A rule [pattern] = [replacement]
  • add zero x = x - adds a new rule that replaces add zero $0, wherever it is found, with $0.
  • add (succ x) y = succ (add x y) - adds a new rule that replaces add (succ $0) $1 with succ (add $0 $1).
  • Patterns must consist of a plain declaration applied to some number of expressions (only involving application). Unrecognized identifiers will be treated as variables for the pattern to match against.
  • All patterns must be possible to match against purely by inspecting the arguments to the plain declaration against axioms.
    Patterns such as add x x are invalid since they would require the pattern matcher to check for equality between two captures of type U64. Patterns like add (add x y) z are similarly illegal.
    The compiler does, however, allow patterns to repeat variables or match against plain declarations when this is the only way for the pattern to be well-typed - as can happen when matching dependent types. It will issue an error in all other cases.
• A let expresion let [name] = [value]; or let [name] : [type] = [value];.
  • let x = add 5 12; - create a new value "x" with the value 17.
  • let x : Vector U64 = [] - create a new value "x" with the specified type and value.