583 lines
11 KiB
Markdown
583 lines
11 KiB
Markdown
# View Contract Syntax Design
|
|
|
|
## 1. Purpose
|
|
|
|
This document specifies source-level syntax sugar for emitting View Contract
|
|
metadata from annotated `tricu` definitions.
|
|
|
|
The syntax is frontend sugar. It lowers to ordinary typed-program nodes consumed
|
|
by the portable checker in `lib/view.tri` and catalog helpers in
|
|
`lib/views/catalog.tri`.
|
|
|
|
The checker remains independent of source syntax.
|
|
|
|
## 2. Definition Annotations
|
|
|
|
A definition may carry argument and return view annotations directly in its head.
|
|
|
|
```tri
|
|
name arg1@Type1 arg2@Type2 =@ReturnType body
|
|
```
|
|
|
|
This declares:
|
|
|
|
```text
|
|
name : Fn [Type1 Type2] ReturnType
|
|
arg1 : Type1
|
|
arg2 : Type2
|
|
```
|
|
|
|
and lowers to View Contract metadata:
|
|
|
|
```tri
|
|
typedDeclareFn nameSym [(Type1) (Type2)] ReturnType t
|
|
typedValue arg1Sym Type1 t
|
|
typedValue arg2Sym Type2 t
|
|
```
|
|
|
|
If body flow metadata is emitted, the body result is required to satisfy the
|
|
appropriate residual view.
|
|
|
|
## 3. Syntax Forms
|
|
|
|
### 3.1 Binder annotation
|
|
|
|
```tri
|
|
x@Bool
|
|
xs@(List Bool)
|
|
f@(Fn [Bool] String)
|
|
```
|
|
|
|
A binder annotation introduces a normal term binder and contributes an argument
|
|
view to the function contract.
|
|
|
|
### 3.2 Phantom argument annotation
|
|
|
|
```tri
|
|
name @A @B =@C body
|
|
```
|
|
|
|
A phantom argument annotation contributes an argument view to the function
|
|
contract but introduces no term binder.
|
|
|
|
This is useful for point-free and combinator-heavy definitions.
|
|
|
|
```tri
|
|
name @A @B =@C body
|
|
```
|
|
|
|
declares:
|
|
|
|
```text
|
|
name : Fn [A B] C
|
|
```
|
|
|
|
The body itself must satisfy the residual function view:
|
|
|
|
```text
|
|
Fn [A B] C
|
|
```
|
|
|
|
### 3.3 Binder prefix with phantom tail
|
|
|
|
Phantom annotations may appear after binder annotations:
|
|
|
|
```tri
|
|
name x@A @B =@C body
|
|
```
|
|
|
|
This declares:
|
|
|
|
```text
|
|
name : Fn [A B] C
|
|
x : A
|
|
```
|
|
|
|
The body must satisfy:
|
|
|
|
```text
|
|
Fn [B] C
|
|
```
|
|
|
|
This allows a named binder prefix with a point-free tail.
|
|
|
|
### 3.4 Return annotation
|
|
|
|
```tri
|
|
name x@A =@B body
|
|
name =@B body
|
|
```
|
|
|
|
`=@B` contributes the result view.
|
|
|
|
A definition with no arguments and a return annotation is a value contract, not a
|
|
zero-arity function contract:
|
|
|
|
```tri
|
|
name =@Bool body
|
|
```
|
|
|
|
lowers to:
|
|
|
|
```tri
|
|
typedValue nameSym viewBool t
|
|
```
|
|
|
|
not:
|
|
|
|
```tri
|
|
typedDeclareFn nameSym [] viewBool t
|
|
```
|
|
|
|
## 4. Ordering Rule
|
|
|
|
Phantom argument annotations may only appear at the end of the argument list.
|
|
|
|
Valid:
|
|
|
|
```tri
|
|
foo x@A y@B =@C body
|
|
foo @A @B =@C body
|
|
foo x@A @B =@C body
|
|
foo x y@B @C =@D body
|
|
```
|
|
|
|
Invalid:
|
|
|
|
```tri
|
|
foo x@A @B z@C =@D body
|
|
foo @A x@B =@C body
|
|
```
|
|
|
|
Once a phantom `@Type` item appears, no later named binder may appear.
|
|
|
|
## 5. Contract-Bearing Definitions
|
|
|
|
A definition is contract-bearing if its head contains any of:
|
|
|
|
```text
|
|
binder@Type
|
|
@Type
|
|
=@Type
|
|
```
|
|
|
|
Ordinary unannotated definitions do not emit View Contract metadata.
|
|
|
|
```tri
|
|
foo x y = body
|
|
```
|
|
|
|
emits no contract metadata.
|
|
|
|
## 6. Unannotated Binders in Contract-Bearing Heads
|
|
|
|
In a contract-bearing definition, an unannotated binder contributes `Any`.
|
|
|
|
```tri
|
|
foo x y@Bool =@String body
|
|
```
|
|
|
|
means:
|
|
|
|
```text
|
|
foo : Fn [Any Bool] String
|
|
x : Any
|
|
y : Bool
|
|
```
|
|
|
|
This keeps mixed annotation lightweight without emitting contracts for fully
|
|
unannotated definitions.
|
|
|
|
## 7. Missing Return Annotation
|
|
|
|
If a contract-bearing definition has argument annotations but no return
|
|
annotation, the return view defaults to `Any`.
|
|
|
|
```tri
|
|
foo x@Bool = body
|
|
```
|
|
|
|
means:
|
|
|
|
```text
|
|
foo : Fn [Bool] Any
|
|
x : Bool
|
|
```
|
|
|
|
## 8. Type Annotation Grammar
|
|
|
|
Annotations are intentionally small at the attachment site.
|
|
|
|
After `@` or `=@`, the parser accepts either a single atomic view expression or
|
|
a parenthesized compound view expression.
|
|
|
|
Valid:
|
|
|
|
```tri
|
|
x@Bool
|
|
x@(List Bool)
|
|
f@(Fn [Bool] String)
|
|
r@(Result String Bool)
|
|
name =@Bool body
|
|
name =@(List Bool) body
|
|
```
|
|
|
|
These are not structural annotations:
|
|
|
|
```tri
|
|
x@List Bool
|
|
f@Fn [Bool] String
|
|
name =@List Bool body
|
|
```
|
|
|
|
They are parsed according to normal definition-head rules. For example,
|
|
`x@List Bool` means binder `x` has the atomic view expression `List`, followed by
|
|
an unannotated binder named `Bool`. Use parentheses when the annotation itself is
|
|
an application.
|
|
|
|
## 9. Type Grammar
|
|
|
|
View expressions are ordinary value-level expressions in a restricted annotation
|
|
grammar:
|
|
|
|
```text
|
|
ViewExpr
|
|
= name
|
|
| integer
|
|
| [ViewExpr...]
|
|
| ViewExpr ViewExpr
|
|
| (ViewExpr)
|
|
```
|
|
|
|
Built-in names lower to standard view values:
|
|
|
|
```text
|
|
Any -> viewAny
|
|
Bool -> viewBool
|
|
String -> viewString
|
|
Byte -> viewByte
|
|
Unit -> viewUnit
|
|
```
|
|
|
|
Atomic refs lower explicitly. String refs are the preferred user-facing form;
|
|
numeric refs remain available for low-level/generated code:
|
|
|
|
```text
|
|
Ref "Nat" -> viewRef "Nat"
|
|
Ref 10 -> viewRef 10
|
|
```
|
|
|
|
Additional named views and view constructors are ordinary `tricu` values:
|
|
|
|
```tri
|
|
Nat = viewRef "Nat"
|
|
Box a = viewPair (viewRef "Box") a
|
|
|
|
idNat x@Nat =@Nat x
|
|
idBox x@(Box String) =@(Box String) x
|
|
```
|
|
|
|
The frontend resolves names and evaluates view expressions, but well-formedness
|
|
is judged by the self-hosted checker (`wellFormedView?` in `lib/view.tri`).
|
|
Malformed view values are rejected when checked or published.
|
|
|
|
## 10. List Syntax in Types
|
|
|
|
Function argument lists use the source type grammar:
|
|
|
|
```tri
|
|
Fn [Bool String] Unit
|
|
Fn [(List Bool) (Maybe String)] Unit
|
|
```
|
|
|
|
The lowered typed program must still respect ordinary `tricu` list syntax, where
|
|
each list element is parenthesized when needed:
|
|
|
|
```tri
|
|
viewFn [(viewBool) (viewString)] viewUnit
|
|
```
|
|
|
|
## 11. Residual Body View
|
|
|
|
For a contract-bearing definition, the full definition view is always:
|
|
|
|
```text
|
|
Fn [allArgumentViews...] returnView
|
|
```
|
|
|
|
except for nullary value annotations, which use the return view directly.
|
|
|
|
The body obligation depends on how many argument views are represented by named
|
|
binders in the definition head.
|
|
|
|
Let:
|
|
|
|
```text
|
|
argViews = [A B C]
|
|
returnView = R
|
|
binderCount = number of named binders before the phantom tail
|
|
remaining = drop binderCount argViews
|
|
```
|
|
|
|
Then:
|
|
|
|
```text
|
|
bodyRequiredView = residual(remaining, returnView)
|
|
```
|
|
|
|
where:
|
|
|
|
```text
|
|
residual([], R) = R
|
|
residual([A ...], R) = Fn [A ...] R
|
|
```
|
|
|
|
Examples:
|
|
|
|
```tri
|
|
foo x@A y@B =@C body
|
|
```
|
|
|
|
Body required view:
|
|
|
|
```text
|
|
C
|
|
```
|
|
|
|
```tri
|
|
foo @A @B =@C body
|
|
```
|
|
|
|
Body required view:
|
|
|
|
```text
|
|
Fn [A B] C
|
|
```
|
|
|
|
```tri
|
|
foo x@A @B =@C body
|
|
```
|
|
|
|
Body required view:
|
|
|
|
```text
|
|
Fn [B] C
|
|
```
|
|
|
|
## 12. Lowering Examples
|
|
|
|
### 12.1 Fully annotated binders
|
|
|
|
Source:
|
|
|
|
```tri
|
|
foo x@Bool xs@(List Bool) =@String body
|
|
```
|
|
|
|
Definition contract:
|
|
|
|
```tri
|
|
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
|
|
typedValue xSym viewBool t
|
|
typedValue xsSym (viewList viewBool) t
|
|
```
|
|
|
|
Body obligation:
|
|
|
|
```tri
|
|
typedRequire bodySym viewString t
|
|
```
|
|
|
|
### 12.2 Pure phantom signature
|
|
|
|
Source:
|
|
|
|
```tri
|
|
foo @Bool @(List Bool) =@String body
|
|
```
|
|
|
|
Definition contract:
|
|
|
|
```tri
|
|
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
|
|
```
|
|
|
|
Body obligation:
|
|
|
|
```tri
|
|
typedRequire bodySym (viewFn [(viewBool) (viewList viewBool)] viewString) t
|
|
```
|
|
|
|
### 12.3 Binder prefix with phantom tail
|
|
|
|
Source:
|
|
|
|
```tri
|
|
foo x@Bool @(List Bool) =@String body
|
|
```
|
|
|
|
Definition contract:
|
|
|
|
```tri
|
|
typedDeclareFn fooSym [(viewBool) (viewList viewBool)] viewString t
|
|
typedValue xSym viewBool t
|
|
```
|
|
|
|
Body obligation:
|
|
|
|
```tri
|
|
typedRequire bodySym (viewFn [(viewList viewBool)] viewString) t
|
|
```
|
|
|
|
### 12.4 Value annotation
|
|
|
|
Source:
|
|
|
|
```tri
|
|
message =@String "hello"
|
|
```
|
|
|
|
Definition contract:
|
|
|
|
```tri
|
|
typedValue messageSym viewString t
|
|
```
|
|
|
|
Body obligation:
|
|
|
|
```tri
|
|
typedRequire bodySym viewString t
|
|
```
|
|
|
|
## 13. `tricu check`
|
|
|
|
`tricu check` consumes an annotated program, lowers annotations to typed program
|
|
metadata, runs the checker, and reports either `ok` or rendered diagnostics.
|
|
|
|
Initial behavior:
|
|
|
|
```bash
|
|
tricu check path/to/program.tri
|
|
```
|
|
|
|
outputs checker success or errors. Diagnostics are rendered by the portable
|
|
checker, then annotated by the frontend with source/debug labels when available:
|
|
|
|
```tri
|
|
id x@String =@Bool x
|
|
```
|
|
|
|
reports:
|
|
|
|
```text
|
|
symbol 1 (x) expected Bool but got String
|
|
```
|
|
|
|
Application result labels include the application head when known:
|
|
|
|
```tri
|
|
xs =@(List String) [(g "hi")]
|
|
g y@String =@Bool y
|
|
```
|
|
|
|
reports:
|
|
|
|
```text
|
|
symbol 3 (g application result) expected String but got Bool
|
|
```
|
|
|
|
These labels are presentation-only metadata. The checker still judges only the
|
|
emitted typed-program evidence.
|
|
|
|
Future behavior may include:
|
|
|
|
```bash
|
|
tricu check --out path/to/executable.arboricx path/to/program.tri
|
|
```
|
|
|
|
which checks an annotated source program and emits an executable Arboricx bundle.
|
|
|
|
The checker library remains available independently of the CLI workflow.
|
|
|
|
## 14. Frontend Lowering Boundaries
|
|
|
|
The annotation syntax is frontend sugar. The canonical checker input remains a
|
|
plain typed program: ordinary `typedValue`, `typedDeclareFn`,
|
|
`typedRequire`, and `typedApply` nodes represented as portable `tricu`
|
|
data.
|
|
|
|
The frontend may emit richer evidence from source forms, but it does not decide
|
|
semantic compatibility. In short:
|
|
|
|
```text
|
|
Haskell emits evidence.
|
|
tricu judges evidence.
|
|
```
|
|
|
|
Current source-driven evidence includes:
|
|
|
|
- literal views for strings, bytes, unit, and homogeneous list literals;
|
|
- expected element requirements for `List T` bodies;
|
|
- expected `Fn` requirements for lambda literals and curried application spines;
|
|
- application argument requirements when the callee has a known `Fn` view;
|
|
- expected constructor flow for unshadowed stdlib constructors:
|
|
- `pair` with expected `Pair A B`;
|
|
- `just` and `nothing` with expected `Maybe A`;
|
|
- `ok` and `err` with expected `Result E A`.
|
|
|
|
Constructor lowering only applies when the constructor name is not shadowed by a
|
|
local binder or top-level definition in the checked source. If a program defines
|
|
its own `pair`, `just`, `nothing`, `ok`, or `err`, checking falls back to normal
|
|
application evidence.
|
|
|
|
For tooling and regression tests, the frontend exposes a lowering-only API that
|
|
returns emitted typed program text without invoking the checker:
|
|
|
|
```hs
|
|
lowerSource :: String -> Either String String
|
|
```
|
|
|
|
It also exposes debug labels for symbols:
|
|
|
|
```hs
|
|
lowerSourceWithDebug :: String -> Either String (String, Map Integer String)
|
|
```
|
|
|
|
Debug labels are presentation metadata only. They are not part of checker
|
|
semantics and are not consumed by `lib/view.tri`.
|
|
|
|
`do` blocks have no separate View Contract semantics. The parser lowers them
|
|
through their explicit bind operator:
|
|
|
|
```tri
|
|
do bind
|
|
x <- action
|
|
next x
|
|
```
|
|
|
|
becomes ordinary application/lambda structure. Checking then follows the known
|
|
`Fn` view of the bind operator, including the callback argument view when it is
|
|
available.
|
|
|
|
## 15. Summary
|
|
|
|
The annotation syntax is:
|
|
|
|
```tri
|
|
name arg@A arg2@B =@C body
|
|
name @A @B =@C body
|
|
name arg@A @B =@C body
|
|
name =@C body
|
|
```
|
|
|
|
Core rules:
|
|
|
|
1. Binder annotations introduce binders and argument views.
|
|
2. Phantom annotations introduce argument views only.
|
|
3. Phantom annotations may only appear after all binders.
|
|
4. Unannotated binders in contract-bearing heads contribute `Any`.
|
|
5. Missing return annotations in contract-bearing heads default to `Any`.
|
|
6. Nullary `=@T` definitions are value contracts, not zero-arity functions.
|
|
7. Compound annotation types must be parenthesized.
|
|
8. Lowering emits ordinary typed-program nodes for the existing checker.
|