Contract Types Guide

Status: Not yet implemented -- requires -Xcontracts flag (planned for v4).

For runtime contract macros available today (assert!, require!, ensure!, invariant!), see Error Handling Guide.

Contract types add runtime-checked predicates to types as a first-class language feature. A contract type { x : T | p } represents values of type T that satisfy predicate p, verified automatically at function boundaries and assignment sites.

Overview

The existing assert!, require!, and ensure! macros in stdlib/contract.tur are imperative guards -- you place them manually inside function bodies. Contract types are declarative annotations: you write the predicate in the type, and the compiler inserts the checks at every crossing point.

Contract predicates are ordinary Turmeric expressions -- no special syntax beyond the { x : T | p } wrapper. They are pure by default; the elaborator enforces #{} on all predicate expressions.

Syntax

Inline Contract Type

;; A non-negative integer
(deftype Nat { x : int | (>= x 0) })

;; Inline in a function signature
(defn sqrt [x : { y : double | (>= y 0) }] : double
  ...)

;; A non-negative integer
deftype Nat { x : int | {x >= 0} }

;; Inline in a function signature
defn sqrt [x : { y : double | {y >= 0} }] : double
  ...

The bound variable (x, y) is local to the predicate expression. It refers to the value being checked, not to any name in the surrounding scope.

Pre- and Post-Conditions

(defn divide [x : int, y : int] : int
  :pre  (!= y 0)
  :post (= (* result y) x)
  (/ x y))

defn divide [x : int, y : int] : int
  :pre  {y != 0}
  :post {(* result y) = x}
  {x / y}

• :pre -- checked at function entry, before any user code runs.
• :post -- checked before each return; the return value is bound to result inside the predicate expression.

Contract on a defn

(defn safe-sqrt [x : double] : double
  :pre  (>= x 0.0)
  :post (>= result 0.0)
  (sqrt x))

defn safe-sqrt [x : double] : double
  :pre  {x >= 0.0}
  :post {result >= 0.0}
  sqrt(x)

Contract on a Struct Field

(defstruct BoundedBuffer [
  data  : (vec int)
  index : { i : int | (and (>= i 0) (< i (vec/len data))) }])

defstruct BoundedBuffer [
  data  : (vec int)
  index : { i : int | and({i >= 0} {i < vec/len(data)}) }]

The predicate for a struct field may reference other fields in scope at elaboration time.

FFI Contract

(extern-c sqlite3_column_int [stmt : ptr, col : int] : int
  :pre  (and (!= stmt null) (>= col 0))
  :post (>= result 0))

extern-c sqlite3_column_int [stmt : ptr, col : int] : int
  :pre  and({stmt != null} {col >= 0})
  :post {result >= 0}

Examples

Bounds-Checked Vector Access

The contract documents and enforces the requirement at the call site. Inside the body, no redundant check is needed:

(defn vec-get-checked [v : (vec a), i : { x : int | (and (>= x 0) (< x (vec/len v))) }] : a
  (vec/get-unsafe v i))

;; At the call site, the elaborator inserts:
;;   assert((3 >= 0) && (3 < vec_len(v)), "contract violated: i in bounds")
;;   vec_get_unsafe(v, 3)
(defn example [v : (vec int)] : int
  (vec-get-checked v 3))

defn vec-get-checked [v : (vec a), i : { x : int | and({x >= 0} {x < vec/len(v)}) }] : a
  vec/get-unsafe(v i)

;; At the call site, the elaborator inserts:
;;   assert((3 >= 0) && (3 < vec_len(v)), "contract violated: i in bounds")
;;   vec_get_unsafe(v, 3)
defn example [v : (vec int)] : int
  vec-get-checked(v 3)

Gradual Typing with Contracts

Accept an untyped value and narrow it at runtime:

(defn ensure-positive [x : any] : { y : int | (>= y 0) }
  :contract (>= x 0)
  x)

(defn pipeline [] : { y : int | (>= y 0) }
  (ensure-positive 42))

defn ensure-positive [x : any] : { y : int | {y >= 0} }
  :contract {x >= 0}
  x

defn pipeline [] : { y : int | {y >= 0} }
  ensure-positive(42)

API Boundary Validation via FFI

Contracts are checked before the C call and on return:

(extern-c sqlite3_column_int [stmt : ptr, col : int] : int
  :pre  (and (!= stmt null) (>= col 0))
  :post (>= result 0))

extern-c sqlite3_column_int [stmt : ptr, col : int] : int
  :pre  and({stmt != null} {col >= 0})
  :post {result >= 0}

Pre- and Post-Conditions

(defn safe-sqrt [x : double] : double
  :pre  (>= x 0.0)
  :post (>= result 0.0)
  (sqrt x))

defn safe-sqrt [x : double] : double
  :pre  {x >= 0.0}
  :post {result >= 0.0}
  sqrt(x)

Where Checks Are Inserted

Contract Failure

By default, a violated contract calls panic. A custom handler can be registered:

(set-contract-handler! (fn [msg location] : unit
  (log/error (str "Contract violated at " location ": " msg))))

set-contract-handler!(fn [msg location] : unit
  log/error $ str("Contract violated at " location ": " msg))

For scoped overrides:

(with-contract-handler my-handler
  (do-something-with-contracts))

with-contract-handler my-handler
  do-something-with-contracts()

Feature Flag and Build Modes

Enable contract types with the -Xcontracts flag:

turc -Xcontracts myfile.tur

Contracts are compile-time insertions. A release build with no flag produces the same binary as code written without contract annotations.

Error Codes

Run tur explain TUR_E0400 for full diagnostic output with source location and predicate text.

Interaction with Existing Features

Contract Types vs. Contract Macros

Use contract macros when: - Adding a one-off sanity check inside a function body - The check is only relevant in a specific branch, not at all entry points - You want imperative control over exactly where the check runs

Use contract types when: - The predicate is part of the type's meaning (e.g. "a non-negative integer") - You want the compiler to enforce the check at every call site automatically - Writing a library API where callers should be told the invariant upfront - Validating at FFI boundaries

Implementation Phases

Contract types are planned in four phases:

See Also

• Error Handling Guide -- Result, Option, panic, and today's contract macros
• C Integration Guide -- FFI and extern-c
• Type Annotations Guide -- compound type syntax
• Advanced Type System Rationale -- why contract types shipped and refinement types were deferred