329 lines
8.8 KiB
Markdown
329 lines
8.8 KiB
Markdown
# Contract Kernel Design
|
|
|
|
## Status
|
|
|
|
Implemented. The contract system uses a configurable kernel defined in
|
|
`lib/base.tri`. All contract logic lives in pure tree calculus.
|
|
|
|
## Goals
|
|
|
|
1. **User code stays ergonomic.** `@`/`=@` syntax remains. Calling a guarded
|
|
function looks the same as calling an unguarded one.
|
|
2. **No stringly-dynamic failures.** A contract boundary returns a structured
|
|
`Result`. The kernel decides whether to abort, resume with a replacement,
|
|
log, or otherwise transform the result.
|
|
3. **All evaluation logic in pure tree calculus.** The evaluator does not treat
|
|
contracts specially; contracts are ordinary functions and the desugarer
|
|
emits ordinary tricu code.
|
|
4. **Optional contract enforcement.** A CLI/REPL flag can disable contract
|
|
syntax entirely by stripping annotations at desugar time.
|
|
5. **Configurable failure semantics.** A global kernel, supplied by the user
|
|
via CLI/REPL, determines how contract failures are handled for the
|
|
session.
|
|
|
|
## Core idea
|
|
|
|
A contract annotation on a definition desugars into a runtime guard. The
|
|
runtime guard applies a contract predicate to a value and passes the resulting
|
|
`Result` to the current `kernel`. The `kernel` returns another `Result`, which
|
|
the wrapper inspects:
|
|
|
|
- `ok value` means the guard succeeded; continue with `value`.
|
|
- `err msg` means the guard failed; abort and propagate the error.
|
|
|
|
The default kernel is the identity on the contract `Result`. A custom kernel
|
|
can transform failures into successes, wrap diagnostics, or log failures before
|
|
aborting.
|
|
|
|
## Kernel
|
|
|
|
### Signature
|
|
|
|
```tricu
|
|
kernel contract value result -> Result
|
|
```
|
|
|
|
- `contract`: the contract predicate being checked.
|
|
- `value`: the unevaluated original value passed to the contract.
|
|
- `result`: the `Result` produced by evaluating `contract value t`.
|
|
|
|
### Default kernel
|
|
|
|
`lib/base.tri` defines both `defaultKernel` and the active `kernel`:
|
|
|
|
```tricu
|
|
defaultKernel = (contract value result :
|
|
matchResult
|
|
(msg rest : err msg rest)
|
|
(v rest : ok v rest)
|
|
result)
|
|
|
|
kernel = defaultKernel
|
|
```
|
|
|
|
The runner may rebind `kernel` to a different value before evaluating user
|
|
code (e.g. via `--contract-kernel`). Because `withContract` looks up `kernel`
|
|
dynamically at application time, rebinding it changes the behaviour of every
|
|
contract boundary.
|
|
|
|
### Skip kernel
|
|
|
|
Resume with the original value whenever a contract fails:
|
|
|
|
```tricu
|
|
skipKernel = (contract value result :
|
|
matchResult
|
|
(msg rest : ok value rest)
|
|
(v rest : ok v rest)
|
|
result)
|
|
```
|
|
|
|
### Logging kernel
|
|
|
|
Abort but also emit a log entry:
|
|
|
|
```tricu
|
|
loggingKernel = (contract value result :
|
|
matchResult
|
|
(msg rest : pair (logMsg msg) (err msg rest))
|
|
(v rest : ok v rest)
|
|
result)
|
|
```
|
|
|
|
### Resume-with-default kernel
|
|
|
|
```tricu
|
|
resumeWithZero = (contract value result :
|
|
matchResult
|
|
(msg rest : ok 0 rest)
|
|
(v rest : ok v rest)
|
|
result)
|
|
```
|
|
|
|
## Runtime guard primitive
|
|
|
|
`withContract` is the primitive emitted by the desugarer:
|
|
|
|
```tricu
|
|
withContract = (contract value :
|
|
kernel contract value (contract value t))
|
|
```
|
|
|
|
`check` is a convenience wrapper that extracts the value or the diagnostic
|
|
message:
|
|
|
|
```tricu
|
|
check contract value =
|
|
matchResult
|
|
(msg _ : msg)
|
|
(v _ : v)
|
|
(withContract contract value)
|
|
```
|
|
|
|
## Desugaring
|
|
|
|
Desugaring runs **before** import selection so that names introduced by the
|
|
desugarer (`withContract`, `matchResult`, `err`, `ok`, etc.) are included in
|
|
the selected exports of imported modules. This ensures that a module using
|
|
contract annotations imports everything it needs from `base`/`prelude`.
|
|
|
|
### Phantom annotations
|
|
|
|
```tricu
|
|
add @nat? @nat? =@nat? addRaw
|
|
```
|
|
|
|
desugars to:
|
|
|
|
```tricu
|
|
add = (x y :
|
|
matchResult
|
|
(msg _ : \_ : err msg t)
|
|
(x' _ :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(y' _ :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(r _ : r)
|
|
(withContract nat? (addRaw x' y')))
|
|
(withContract nat? y))
|
|
(withContract nat? x))
|
|
```
|
|
|
|
The first failure continuation is absorbing (`\_ : err msg t`) because `add`
|
|
is curried and a failure on the first argument should consume the second
|
|
argument without producing garbage.
|
|
|
|
`addRaw` is the locally-let-bound raw helper, as in the current phantom
|
|
implementation.
|
|
|
|
### Named-binder annotations
|
|
|
|
```tricu
|
|
safeDiv a@nat? b@(andC nat? nonZero?) =@nat? div a b
|
|
```
|
|
|
|
desugars to:
|
|
|
|
```tricu
|
|
safeDiv = (a b :
|
|
matchResult
|
|
(msg _ : \_ : err msg t)
|
|
(a' _ :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(b' _ :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(r _ : r)
|
|
(withContract nat? (div a' b')))
|
|
(withContract (andC nat? nonZero?) b))
|
|
(withContract nat? a))
|
|
```
|
|
|
|
### No return contract
|
|
|
|
```tricu
|
|
head xs@(nonEmptyListOf anyC) =@anyC headRaw
|
|
```
|
|
|
|
desugars to:
|
|
|
|
```tricu
|
|
head = (xs :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(xs' _ :
|
|
matchResult
|
|
(msg _ : err msg t)
|
|
(r _ : r)
|
|
(withContract anyC (headRaw xs')))
|
|
(withContract (nonEmptyListOf anyC) xs))
|
|
```
|
|
|
|
### No annotations
|
|
|
|
Definitions without `@`/`=@` are emitted unchanged.
|
|
|
|
## Failure propagation
|
|
|
|
When a non-final argument contract fails, the wrapper returns a function that
|
|
absorbs the next argument and then returns the failed `Result`. This prevents
|
|
partial-application accidents like `gt? "the" 3` reducing to a garbage number.
|
|
|
|
When the final argument or result contract fails, the wrapper returns
|
|
`\msg -> err msg t`, which is the failure constructor awaiting its `rest`
|
|
slot.
|
|
|
|
## Skip-contracts flag
|
|
|
|
When the `--skip-contracts` flag is set, the desugarer strips all `@`/`=@`
|
|
annotations and emits the raw function body. This is faster than running the
|
|
skip kernel because no contract code is generated at all.
|
|
|
|
### CLI
|
|
|
|
```bash
|
|
tricu eval --skip-contracts program.tri
|
|
tricu repl --skip-contracts
|
|
```
|
|
|
|
### REPL
|
|
|
|
```tricu
|
|
> :set skip-contracts
|
|
> add 1 2
|
|
3
|
|
> :unset skip-contracts
|
|
> add "bad" 2
|
|
[t, "not a natural number"]
|
|
```
|
|
|
|
## Kernel selection
|
|
|
|
### CLI
|
|
|
|
```bash
|
|
tricu eval --contract-kernel resumeWithZero program.tri
|
|
```
|
|
|
|
### REPL
|
|
|
|
```tricu
|
|
> :set contract-kernel resumeWithZero
|
|
> add "bad" 2
|
|
2
|
|
```
|
|
|
|
### Resolution
|
|
|
|
The kernel name is resolved like any other top-level binding in the program or
|
|
its imports. The runner prepends `kernel = <name>` to the program AST (or
|
|
inserts it into the environment) after imports are resolved. If the name is
|
|
not found, evaluation fails with an undefined-variable error.
|
|
|
|
## Base library changes
|
|
|
|
1. `withContract` becomes the runtime guard primitive shown above.
|
|
2. `check` extracts the checked value or diagnostic message from the kernel
|
|
`Result`.
|
|
3. Contract predicates (`nat?`, `nonZero?`, `bool?`, etc.) remain pure
|
|
functions returning `Result`.
|
|
4. Guarded base functions (`add`, `sub`, `head`, `div`, etc.) use the new
|
|
desugaring.
|
|
5. Raw helpers (`addRaw`, `subRaw`, etc.) remain for internal use and recursion.
|
|
|
|
## Custom contracts
|
|
|
|
Users write ordinary predicates returning `Result`:
|
|
|
|
```tricu
|
|
positive? = (n rest :
|
|
ifThenElse (gte? n 1)
|
|
(ok n rest)
|
|
(err "expected positive integer" rest))
|
|
```
|
|
|
|
and use them with the same syntax:
|
|
|
|
```tricu
|
|
fact n@positive? =@nat? y (self n : ...)
|
|
```
|
|
|
|
Contract combinators (`andC`, `orC`, `guardC`) compose in the obvious way.
|
|
|
|
## Limitations
|
|
|
|
1. **Global kernel only.** There is no local kernel override. A module or
|
|
function cannot install a different kernel for part of the program.
|
|
Workarounds: split into separate evaluation sessions, or use explicit
|
|
`withContract` calls with a local handler function.
|
|
2. **Kernel must return `Result`.** A kernel that returns a plain value is a
|
|
bug. The `defaultKernel`/`skipKernel` templates show the required shape.
|
|
3. **Failures are first-class `Result` values.** A caller that ignores a
|
|
returned `err msg` and treats it as data will operate on the `Result` tree.
|
|
This is inherent to any value-level error mechanism.
|
|
4. **Function contracts are advanced.** Contracts on function arguments
|
|
(e.g. `f @ (nat? -> nat?)`) require intensional/quantified contracts. The
|
|
simple predicate model covers most use cases.
|
|
|
|
## Implementation notes
|
|
|
|
- `Frontend.ContractDesugar` emits `matchResult`/`withContract`/`err`/`ok`
|
|
instead of continuation-passing `withContract`.
|
|
- `FileEval.loadFile'` desugars before computing selected exports, so
|
|
imported modules bring in the runtime helpers needed by annotations.
|
|
- `Eval.injectKernel` is a fallback that binds `kernel` to `defaultKernel`
|
|
when `kernel` is missing from the environment.
|
|
|
|
## Open questions
|
|
|
|
1. **Should `--skip-contracts` strip annotations or just bind the skip
|
|
kernel?** Currently stripping is the intended design; not yet implemented.
|
|
2. **Should we provide a small set of built-in kernel names?** `default`,
|
|
`skip`, `strict`, `log` would cover common cases without requiring the user
|
|
to define them.
|
|
3. **How do we expose the current kernel to introspection?** A top-level
|
|
`currentContractKernel` binding might be useful for debugging.
|