327 lines
8.9 KiB
Markdown
327 lines
8.9 KiB
Markdown
# Contracts
|
|
|
|
Contracts are the portable runtime boundary-checking layer for `tricu`. A
|
|
contract is an ordinary `tricu` function that inspects a value and returns a
|
|
standard `Result`.
|
|
|
|
Contracts are not a type system. Tree Calculus is intensional: every value is a
|
|
tree and can be inspected by any function. A contract can only observe a value
|
|
and fail when it does not satisfy the advertised predicate. It cannot hide a
|
|
value's representation or prove that an opaque function behaves correctly for
|
|
all inputs.
|
|
|
|
Static typing for Tree Calculus is an area of active research. This document
|
|
describes the dynamic-contract layer that exists today and the guarantees it
|
|
can honestly claim.
|
|
|
|
## 1. The contract type
|
|
|
|
A contract is a function:
|
|
|
|
```tri
|
|
contract : Tree -> Tree -> Result Tree Tree
|
|
```
|
|
|
|
The second argument is the conventional `rest` slot. It takes a value and a rest
|
|
and returns one of the standard `Result` shapes from `lib/base.tri`:
|
|
|
|
```tri
|
|
ok value rest = pair true (pair value rest)
|
|
err msg rest = pair false (pair msg rest)
|
|
```
|
|
|
|
In contract contexts the `rest` slot is conventionally `t`. Two helpers make
|
|
this explicit:
|
|
|
|
```tri
|
|
contractOk = (value : (rest : ok value rest))
|
|
contractErr = (msg : (rest : err msg rest))
|
|
```
|
|
|
|
- On success, a contract returns the checked value. This may be the original
|
|
value or a transformed/normalized value.
|
|
- On failure, it returns a reason. The reason is an arbitrary tree, often a
|
|
string or a structured diagnostic.
|
|
|
|
Because a contract is just a tree-valued function, any Tree Calculus
|
|
implementation can apply it. No special contract object format is required.
|
|
|
|
## 2. Core boundary wrappers
|
|
|
|
### 2.1 Explicit check
|
|
|
|
`checkContract` applies a contract with the conventional `t` rest slot and
|
|
returns the raw `Result`:
|
|
|
|
```tri
|
|
checkContract = (contract value : contract value t)
|
|
```
|
|
|
|
This is the most flexible form. The caller decides what to do with failure.
|
|
|
|
### 2.2 Direct boundary abort
|
|
|
|
`withContract` applies a contract with the conventional `t` rest slot and
|
|
continues on success, or calls a failure continuation on failure:
|
|
|
|
```tri
|
|
withContract = (contract value onOk onFail :
|
|
matchResult
|
|
(msg _ : onFail msg)
|
|
(checked _ : onOk checked)
|
|
(contract value t))
|
|
```
|
|
|
|
The failure continuation is supplied by the host or by the surrounding program.
|
|
It may abort, log, return a default, or raise an effect. The core contract
|
|
standard does not prescribe the failure behavior.
|
|
|
|
### 2.3 Example: a simple contract
|
|
|
|
```tri
|
|
isZero? = n :
|
|
equal? n 0
|
|
|
|
nat? = guardC "not a natural number" (n : gte? n 0)
|
|
|
|
-- explicit check
|
|
result = checkContract nat? 5
|
|
|
|
-- boundary abort
|
|
five = withContract nat? 5 (x : x) (msg : 0)
|
|
```
|
|
|
|
Real contract predicates are usually more interesting than `isZero?`; this
|
|
illustrates only the shape.
|
|
|
|
## 3. Contract combinators
|
|
|
|
Contracts compose using ordinary `tricu` functions. A few common patterns:
|
|
|
|
```tri
|
|
andC = (c1 c2 value rest :
|
|
matchResult
|
|
(msg _ : contractErr msg rest)
|
|
(v _ : c2 v rest)
|
|
(c1 value rest))
|
|
|
|
mapC = (f c value rest :
|
|
matchResult
|
|
(msg _ : contractErr msg rest)
|
|
(v _ : contractOk (f v) rest)
|
|
(c value rest))
|
|
|
|
listOf = (c xs rest : ...) -- checks spine and element contract
|
|
pairOf = (c1 c2 p rest : ...)
|
|
```
|
|
|
|
These are library code, not core standard. A contract library can provide
|
|
`listOf`, `pairOf`, `fnContract`, and similar helpers.
|
|
|
|
## 4. Higher-order contracts
|
|
|
|
A contract for a function value returns a wrapped proxy. The proxy itself is a
|
|
contract: it checks arguments on the way in and results on the way out.
|
|
|
|
```tri
|
|
fnContract = (argC resC f rest :
|
|
contractOk
|
|
(x : (rest1 :
|
|
withContract argC x
|
|
(x' :
|
|
withContract resC (f x')
|
|
(y : contractOk y rest1)
|
|
(msg : contractErr msg rest1))
|
|
(msg : contractErr msg rest1)))
|
|
rest)
|
|
```
|
|
|
|
This does not prove that `f` is well-behaved internally; it only catches
|
|
violations at observed calls.
|
|
|
|
## 5. Interaction-tree contract effects
|
|
|
|
The core contract layer returns `Result`. For code that wants catchable,
|
|
composable contract failures without threading `Result` through every function,
|
|
contracts can be lifted into an interaction tree.
|
|
|
|
### 5.1 Interaction-tree constructors
|
|
|
|
These reuse the same `pure`/`bind` tags already used for `tricu` IO:
|
|
|
|
```tri
|
|
pureE value = pair 0 value
|
|
bindE action k = pair 1 (pair action k)
|
|
exceptE tag value k = pair 2 (pair tag (pair value k))
|
|
```
|
|
|
|
`exceptE` is resumable: `k` is the continuation. A handler may resume with
|
|
`k replacement` or abort by ignoring `k`. Contract failures usually abort; the
|
|
resumable shape is provided for generality and for richer effect handlers.
|
|
|
|
### 5.2 Lifting a contract
|
|
|
|
```tri
|
|
checkM contract value =
|
|
matchResult
|
|
(msg _ : exceptE "contract" msg (\_ : pureE t))
|
|
(checked _ : pureE checked)
|
|
(contract value t)
|
|
```
|
|
|
|
`pureM` and `bindM` are aliases for `pureE` and `bindE`:
|
|
|
|
```tri
|
|
pureM = pureE
|
|
bindM = bindE
|
|
```
|
|
|
|
### 5.3 Lifting pure functions
|
|
|
|
```tri
|
|
liftM f = (x : pureE (f x))
|
|
```
|
|
|
|
### 5.4 Example
|
|
|
|
```tri
|
|
halfM n =
|
|
bindM (checkM even? n)
|
|
(\n' : pureM (div n' 2))
|
|
|
|
use =
|
|
handleM "contract"
|
|
(\msg k : pureM 0)
|
|
(halfM 5)
|
|
```
|
|
|
|
`handleM` is a pure tree-to-tree function that interprets `exceptE` nodes,
|
|
either resuming with a replacement value or returning a failure tree.
|
|
|
|
### 5.5 Running a pure interaction tree
|
|
|
|
```tri
|
|
runM tree =
|
|
-- interprets pureE, bindE, and exceptE nodes
|
|
-- returns a Result or a residual effect tree
|
|
...
|
|
```
|
|
|
|
If the tree contains no IO or other host effects, `runM` can be written
|
|
entirely in `tricu`.
|
|
|
|
## 6. Source syntax
|
|
|
|
Source annotations are frontend sugar for inserting contract boundaries. They do
|
|
not change the runtime semantics of ordinary code; they tell the frontend where
|
|
to emit contract checks.
|
|
|
|
### 6.1 Argument and result assertions
|
|
|
|
```tri
|
|
idNat x@Nat =@Nat x
|
|
```
|
|
|
|
`x@Nat` inserts a `Nat` contract check on the argument. `=@Nat` inserts a check
|
|
on the result.
|
|
|
|
### 6.2 Compound contracts
|
|
|
|
```tri
|
|
sum xs@(List Nat) =@Nat ...
|
|
useHandler f@(Fn [(NonEmptyList String)] String) =@String ...
|
|
```
|
|
|
|
Compound annotations must be parenthesized when they contain application.
|
|
|
|
### 6.3 Phantom arguments
|
|
|
|
```tri
|
|
map @A @B =@(Fn [(Fn [A] B) (List A)] (List B)) ...
|
|
```
|
|
|
|
A phantom argument contributes a contract to the function boundary without
|
|
introducing a term binder.
|
|
|
|
### 6.4 Missing annotations
|
|
|
|
Unannotated binders in a contract-bearing head default to `Any`. A missing
|
|
return annotation defaults to `Any`.
|
|
|
|
```tri
|
|
foo x y@Bool = body -- foo : Fn [Any Bool] Any, y : Bool
|
|
```
|
|
|
|
### 6.5 Export contracts
|
|
|
|
A module export may advertise a contract:
|
|
|
|
```tri
|
|
!export factorial : Fn [Nat] Nat
|
|
```
|
|
|
|
The advertised contract travels with the export in the module manifest.
|
|
|
|
## 7. Module and content-store integration
|
|
|
|
Contracts attach to module exports as ordinary content-addressed tree terms.
|
|
There is no special contract object kind. The manifest references the contract
|
|
with the same object kind as any other tree term:
|
|
|
|
```text
|
|
name: "factorial"
|
|
object:
|
|
kind: arboricx.tree-term.v1
|
|
hash: <tree-term hash>
|
|
contract:
|
|
kind: arboricx.tree-term.v1
|
|
hash: <contract term hash>
|
|
```
|
|
|
|
The earlier `arboricx.view-contract.type.v1` object kind is removed. A
|
|
contract is just a tree term.
|
|
|
|
For locally built modules, advertised export contracts may be checked before the
|
|
manifest is published. For imported modules, the advertised contract is a
|
|
boundary assumption. The local checker may insert guard wrappers when a
|
|
contracted import is used.
|
|
|
|
See `docs/module-system-design.md` and
|
|
`docs/content-store-and-module-format.md` for the full store, manifest, and
|
|
bundle conventions.
|
|
|
|
## 8. Guarantees
|
|
|
|
The contract layer honestly claims only:
|
|
|
|
1. A contract applied to a value returns a standard `Result` shape.
|
|
2. `withContract` and `checkM` invoke the contract at the represented boundary.
|
|
3. A failed contract invokes the supplied failure continuation or `exceptE`
|
|
node.
|
|
4. Content-addressed references prevent an attached contract from silently
|
|
drifting to a different stored object.
|
|
5. Provenance labels record where a contract assertion came from.
|
|
|
|
Only the contract function itself observes the runtime value. The rest is
|
|
metadata plumbing.
|
|
|
|
## 9. Limitations
|
|
|
|
- Contracts do not establish parametricity or representation independence.
|
|
- They do not prove that opaque recursive or primitive code satisfies its
|
|
contract for every input.
|
|
- They do not remove the need for tests, careful API design, or future static
|
|
analysis.
|
|
- Higher-order contract wrapping has the usual costs and proxy-like behavior
|
|
of dynamic contract systems.
|
|
|
|
## 10. Summary
|
|
|
|
- A contract is an ordinary `tricu` function: `Tree -> Result Tree Tree`.
|
|
- `withContract` aborts at a boundary; `checkContract` returns the raw
|
|
`Result`.
|
|
- The interaction-tree layer (`checkM`, `bindM`, `handleM`) adds catchable,
|
|
composable failures on top of the same core contracts.
|
|
- Contracts attach to module exports as ordinary tree-term objects.
|
|
- Provenance labels record source and blame, but do not prove truth.
|