Simple types

Type Ascriptions

extend with #type-ascriptions;

This extension provides the ability to explicitly ascribe a particular type to a given expression. It adds the syntax expr as Type (where expr is an arbitrary expression and Type is an arbitrary type). Type ascription is useful when it is not possible for the typechecker to infer a unique type for an expression, such as inl(0) (which has the type Nat + T for any arbitrary T).

For example, when typechecking the following:

language core;

extend with #sum-types;

fn main(n : Nat) -> fn(Bool) -> Nat + Bool {
  return (fn (b : Bool) { return inl(n) })(true)
}

it will throw a type error:

ERROR_AMBIGUOUS_SUM_TYPE: type inference for sum types is not supported (use type ascriptions)

Instead, it should be written as such:

language core;

extend with #sum-types;
extend with #type-ascriptions;

fn main(n : Nat) -> Nat + Bool {
  return (fn (b : Bool) { return inl(n) as (Nat + Bool) })(true)
}

It is also similarly useful with variants since an expression of a variant type specifies only a single field, so we cannot fully infer its type.

Note: Do not confuse it with type casting (which has the same syntax in TypeScript)! Type ascriptions still need to be checked by the compiler to be valid and are not to be trusted blindly (as is usually the case with type casting).

Type Aliases

extend with #type-aliases;

Type aliases provide a way of giving different names to types. They are useful when a type is too long to type and needs to be repeated or can have a more descriptive name.

language core;
extend with #type-aliases, #records;

type NonNegative = Nat
type MapEntry = { key : Nat, value : Nat }
type LinkedList = { value : NonNegative, next : LinkedList }

Unit Type

extend with #unit-type;

The unit type is a type that only has one value: the unit. It can be considered a 0-tuple.

language core;
extend with #unit-type;

fn ignore(_ : Nat) -> Unit {
  return unit
}

Pairs

extend with #pairs;

Adds the pair type {A, B} for any types A and B.

Terms:

• {t1, t2} — a pair of terms t1 and t2
• t.1 — accessing the first component of a term t
• t.2 — accessing the second component of a term t

Example:

language core;
extend with #pairs, #arithmetic-operators;

fn add(t : {Nat, Nat}) -> Nat {
  return t.1 + t.2
}

fn main(n : Nat) -> Nat {
  return {succ(n), {succ(succ(n)), n}}.2.1
}

Tuples

extend with #tuples;

A tuple is an immutable, heterogenous, fixed-length list. The length of a tuple must be non-negative. The type of a tuple is a tuple consisting of the types of the elements.

extend with #tuples;

fn noop(_ : {}) -> {} {
  return {}
}

fn third(tup : {Nat, Nat, Nat}) -> Nat {
  return tup.3
}

fn main(n : Nat) -> Nat {
  return third({n, succ(n), succ(succ(n))})
}

Implies: pairs.

Records

extend with #records;

Records are a composite data type that consists of a collection of key-value pairs, similar to struct in C. All keys are known at compile time and must be specified fully when creating values of the particular record type. Fields in the record can be accessed by their name using the dot-notation. Similar to tuples, the type of a record is a record with the same keys and the respective types of the values.

language core;

extend with #records;

fn iterate(n : Nat) -> { current : Nat, next : Nat} {
  return { current = n, next = succ(n) }
}

fn main(n : Nat) -> Nat {
  return iterate(0).next
}

Sum Types

extend with #sum-types;

A sum type represents a data structure that can hold values of different types (that are known at compile-time). For example, a variable with the type Nat + Bool can hold the values true, false, 0, 1, and so on. To construct a value with that type, you use inl for a value with the type on the left of the +, or inr for a value of the type on the right.

language core;

extend with #sum-types, #unit-type;

fn test(first : Bool) -> Nat + Unit {
  return if first then inl(succ(0)) else inr(unit)
}

fn main(input : Bool) -> Nat {
  return match test(input) {
      inl(n) => n
    | inr(_) => 0
  }
}

Sum types can also be nested using parenthesis:

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

fn main(input : Nat + (Bool + (fn (Nat) -> Nat))) -> Nat {
  return match input {
        inl(number) => number
      | inr(inl(false)) => 0
      | inr(inl(true)) => succ(0)
      | inr(inr(fun)) => fun(0)
   }
}

Variants

extend with #variants;

A variant type represents multiple possibilities for the value, each consisting of a label and possibly a value attached to that label.

language core;

extend with #variants, #unit-type, #structural-patterns;

fn attempt(get_one? : Bool) -> <| value : Nat, failure : Unit |> {
  return
    if get_one?
      then <| value = 0 |>
      else <| failure = unit |>
}

fn main(succeed : Bool) -> Nat {
  return match attempt(succeed) {
      <| value = n |> => succ(n)
    | <| failure = unit |> => 0
  }
}

Enumerations

extend with #enumerations;

Lists

extend with #lists;

A list is a homogenous collection of elements of an arbitrary length. Its type is written as [Type], and it is constructed using either the cons expression which accepts the head and the tail to be linked, or using the [expr1, expr2, ...] syntax. The first element of the list can be accessed using List::head, the remaining elements (as a list) using List::tail, and you can check if it's empty using List::isempty.

extend with #lists;
extend with #multiparameter-functions;

fn nonempty(list : [Nat]) -> Bool {
  return if List::isempty(list) then true else false
}

fn first_or_default(list : [Nat], default : Nat) -> Nat {
  return if nonempty(list) then List::head(list) else default
}

fn main(default : Nat) -> Nat {
  return first_or_default([], default)
}