Appendix A: Syntax Quick Reference

A short reference for when you need a reminder.

A.1 Variables, functions, and branches

ap-a1.taut

let x: i64 := 10
var y: i64 := 1
y := y + 1

fn add(a: i64, b: i64): i64 { a + b }
let larger := if x > y { x } else { y }
perform show("larger", larger)

// Bind, update, branch, and call a function.

Execution result

・ add

larger = 10

A.2 Types and data

ap-a2.taut

shared struct Pair2(A: Shared, B: Shared) { first: A, second: B }
shared enum Choice(A: Shared) { None2, Some2(A) }
let p := Pair2 { first: 3, second: "ok" }
perform show("first", p.first)

// Declare shared generic data and read a field.

Execution result

first = 3

Function type parameters use <A>. Type declarations and type applications use parentheses, as in Pair2(A: Shared, B: Shared) and Choice(i64). Shared constrains an argument to values that can be duplicated.

A.3 Ownership and borrowing

ap-a3.taut

import std::prelude::Affine

fn read(&v: Vec(i64)): u64 { Vec::len(&v) }

fn write(&mut v: Vec(i64)): () {
  Vec::push(&mut v, 1)
}

var v := Vec::new()
write(&mut v)
perform show("n", read(&v))

// Borrow a vector for reading or mutation.

Execution result

・ read
・ write

n = 1

Notation	Meaning
`let x := ...`	Bind a value
`var x := ...`	Create a mutable cell
`x := y`	Assign to a cell
`&x`	Read borrow
`&mut x`	Mutable borrow
`let &x := f(&v)`	Bind a view
`copy` / `shared` / `affine` / `linear`	Value-usage rules

A.4 Effects and proofs

ap-a4.taut

import std::Base

effect choose(): i64 resume ω

let out := handle { perform choose() } with {
  choose(), k => k(1) + k(2)
  return v => v
}
perform show("out", out)

theorem id_prop(P: Prop, p: P): P { p }
theorem equal(n: Nat): n = n { Refl }

// Observe an effect result and check two small proofs.

Execution result

✓ theorem id_prop : ∀ P: Prop. (P) -> P
✓ theorem equal : ∀ n: Nat. n = n

out = 3

Notation	Meaning
`! {e}`	Effects left for the caller
`perform e(...)`	Request an effect operation
`handle {...} with {...}`	Handle effect operations
`resume ω`	Permit repeated resumption
`Prop`	Propositions
`x = y`	An equality proposition
`Refl`	Proof by reflexivity
`by rewrite!(e)`	A proof step using equality
`?h`	An unfinished named hole