Language tour

This page walks the whole language surface in one pass. If you have not built the toolchain yet, start with Getting started. For the full detail on contracts, see Contracts and the lifecycle.

Source files and imports

A source file ends in .geas and holds a list of top level declarations: contracts, records, sums, provisional clauses, and imports. A file is a module, and a directory of files is a package.

An import names a module by a dotted path:

import std.math
import std.collections
import std.traits
import std.errors

Imports resolve beside your root file first and then under GEAS_HOME. Every imported file parses into one shared tree, and cycles and duplicate imports are named errors. A module lends another its record and sum shapes, its error sums, its provisional clauses, and its contracts themselves.

Visibility is by package. A declaration is exported by default; a declaration marked internal is invisible outside its own directory and never reaches the tables a foreign host discovers.

Bindings: let and mut

let binds an immutable name, let mut a reassignable one:

let n = 0
let mut xs = [a, b, c]

Value semantics

Composites carry value semantics at every boundary. A let of a composite, an assignment, and a composite read all deep copy, so mutation through one binding is never visible through another. The one place a write lands in place is an assignment target like xs[0] = y, record.field = y, or map[k] = y, which walks to the named slot and writes there while the right side still copies.

The single exception is a signed contract instance. Copies of the handle alias the same instance and equality is identity. It is also the one value that can never cross the C boundary; only its results can.

Records

A record is a product type, a fixed set of named fields:

record Point {
    x: Int
    y: Int
}

You build one with a brace literal on the type’s name and read its fields by name:

let mut p = Point { x: s, y: 0 }
p.y = p.x + 1

Sum types with is either

A sum is a choice between variants, each of which may carry a payload, written is either:

Grade is either Pass(score: Int) or Fail(reason: String) or Skip

You build a variant by naming it, Pass(7) or Skip, and you take it apart with match.

Match

match is an exhaustive expression over sums, Option, Result, and Bool. It must cover every variant, and the checker rejects it otherwise. Each arm binds the payload it matches:

match g {
    Pass(s) -> {
        return Ok("passed")
    }
    Fail(reason) -> {
        return Err(1)
    }
    Skip -> {
        return Ok("skip")
    }
}

A match is an expression, so it can produce a value directly, and a block is a value too: the last expression in a { } is what it evaluates to.

Loops and control flow

if and else are the conditional, while cond { } loops on a condition, for x in list { } walks a list, and break and continue do what you expect. From skeleton/lang.geas:

pledge fizz(n: Int) -> Result<String, Int> {
    if n < 0 {
        return Err(-n)
    }
    let mut i = 0
    let mut out = ""
    while i < n {
        i = i + 1
        if i % 3 == 0 {
            out = out + "f"
            continue
        }
        out = out + "."
    }
    return Ok(out)
}

String + String concatenates. The logical operators short circuit, so a bounds check like i < n && xs[i] == 0 never touches xs[i] when i < n is false.

Result, Option, and the ? operator

Two sums are built in and everywhere. Option<T> is Some(T) or None. Result<T, E> is Ok(T) or Err(E). Every fallible pledge returns one of them, never a bare value and never an exception, because errors in Geas are values.

? is propagation. f(x)? runs a fallible call, returns its Err from the enclosing pledge immediately, and unwraps its Ok otherwise. The callee’s error type must be the enclosing pledge’s error type. Errors as values covers the whole error story.

Contracts in brief

A contract is the unit of Geas the way a function is the unit of most languages. Here is the whole of skeleton/hello.geas:

GreetError is either Empty

contract Greeter {
    vow prefix: String = "hello, "

    pledge greet(name: String) -> Result<String, GreetError> {
        return Ok(prefix + name)
    }

    pledge shout(name: String) -> Result<String, GreetError>
}

A vow is an immutable field, locked the moment the contract is signed. A vow may carry a default, and a host may override it at sign, but nothing inside the contract can assign to it.

A pledge is a callable commitment with a declared return type, and it is a first class element of the language. greet has a body and is concrete. shout has no body and is abstract: the contract cannot be signed until a host binds an implementation for it, which is how a foreign language plugs its own behavior into a Geas contract.

A clause is an internal method. It never leaves its contract and exists so pledges can share logic:

clause compare(a: Int, b: Int) -> Int {
    if a < b { return -1 }
    if a > b { return 1 }
    return 0
}

Contracts also group pledges into subcontracts and write a fulfillment policy over them. Contracts and the lifecycle covers that in full.

Provisional clauses

A provisional clause is Geas’s trait: a named set of clause signatures a contract can promise to satisfy. From std.traits:

provisional clause Comparable {
    clause compare(a: Int, b: Int) -> Int
}

A contract incorporates one and implements its clauses:

contract StdUser {
    incorporate Comparable
    incorporate Loggable

    clause compare(a: Int, b: Int) -> Int { ... }
    clause log_line(msg: String) -> String { ... }
}

An incorporated signature must match its implementation exactly. Once incorporated, the contract is of that provisional clause, and its pledges use the implemented clauses like any internal method.

Cross contract calls

A pledge body can sign another contract, fulfill its pledges, and break it, which is how contracts compose. From skeleton/std_user.geas:

pledge compute(x: Int) -> Result<Int, Int> {
    let ops = MathOps.sign(epsilon: 0.5)
    let r = ops.abs(x)
    ops.break()
    match r {
        Ok(v) -> {
            let gate = IntGate.sign()
            let d = gate.double_pos(v)?
            gate.break()
            return Ok(d)
        }
        Err(_) -> {
            return Err(-1)
        }
    }
}

MathOps.sign(epsilon: 0.5) signs another contract with a vow override, ops.abs(x) fulfills a pledge through method syntax, and ops.break() tears it down. The instance breaks before r is read, and that is safe: a cross contract call copies the result home before the callee dies.

Standalone programs

Geas contracts are usually libraries other languages drive, but Geas also compiles straight to an executable. Declare one Main contract with a run pledge over List<String> returning Result<Int, E>. This is skeleton/main_demo.geas:

DemoError is either BadMood(reason: String) or Empty

contract Main {
    vow greeting: String = "counted"

    pledge run(args: List<String>) -> Result<Int, DemoError> {
        let mut n = 0
        for a in args {
            if a == "fail" {
                return Err(BadMood("asked to fail"))
            }
            n = n + 1
        }
        return Ok(n)
    }
}

geas build --bin links it into a real program. The generated wrapper signs Main, hands argv to run as a List<String>, and maps the result onto the process exit code: Ok(n) becomes the exit code, and an Err renders itself to stderr and exits 1.

geas build --bin main_demo.geas
./target/geas-out/main_demo a b c ; echo $?   # counts its args, exits 3
./target/geas-out/main_demo fail              # takes the Err path, exits 1

Where to go next

Contracts and the lifecycle for the fulfillment policy and the five states.
Errors as values for the whole error model.
The store layer for contracts backed by a database.
Interop for driving a contract from C or Python.
Reference for the normative language rules.