Skip to main content

Function Type Contracts

Function types can carry contracts using a contract { ... } block after the return type. This lets you describe behavior and effects for function values, callbacks, iterators, and higher-order APIs, not just for named function bodies.

Syntax​

type Step = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result > x;
};

Key rules:

  • Parameters must be named so contracts can refer to them.
  • Use result to refer to the return value in ensures.
  • Contract blocks use semicolons after each clause.
  • reads/modifies clauses are allowed to summarize effects.

Where You Can Use Them​

Function type contracts work anywhere a function type appears:

type Worker = (task : Text) -> Nat contract {
  requires task.size() > 0;
  ensures result >= 0;
};

module {
  public func run(f : Worker, t : Text) : Nat {
    f(t)
  };
}

You can also embed them inside module types for dynamic module values. Sector9's verified for-in support relies on this shape for iterator next() methods.

Contract Subtyping​

Contract subtyping is checked by logical implication:

  • requires is contravariant (a function that accepts more inputs can be used where fewer are required)
  • ensures is covariant (a function that guarantees more can be used where fewer are required)
type Weak = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result >= x;
};

type Strong = (x : Nat) -> Nat contract {
  requires x > 0;
  ensures result > x;
};

let f : Strong = ...;
let g : Weak = f;  // OK: Strong implies Weak

Uncontracted Callback Types​

If a function type has no contract, the verifier treats it as pure. The value you pass must be pure (or have a contract with no reads/modifies and trivial requires). If you need impure callbacks, add a type contract and include the appropriate reads/modifies.

When a callback type does include a contract, the passed value must also carry a contract, and its reads/modifies must fit within the callback's frame.

Restrictions​

Type contracts follow the same spec rules as normal contracts, with a few key limits:

  • await is not allowed inside type contracts
  • old() is not allowed inside requires
  • result is not allowed inside requires
  • Only result is allowed as a return binder

Type contracts are verification-only: they do not add runtime checks by themselves.