feat(haskell): Interaction Tree IO
oops, now we have purely modelled IO 🤷
This commit is contained in:
354
docs/io-in-tricu.md
Normal file
354
docs/io-in-tricu.md
Normal file
@@ -0,0 +1,354 @@
|
||||
# IO in tricu
|
||||
|
||||
> Host-interpreted interaction trees in Tree Calculus.
|
||||
|
||||
## Philosophy
|
||||
|
||||
tricu is a pure language. Its runtime consists entirely of the `T` type
|
||||
(`Leaf | Stem T | Fork T T`) and the `apply` reduction rules. Nothing in
|
||||
the calculus can mutate the world, read a file, or talk to a network.
|
||||
|
||||
This document describes how IO is layered *above* the calculus, not baked
|
||||
into it. The mechanism is structurally identical to how strings and integers
|
||||
already work in tricu: source-level constructs that evaluate to pure trees,
|
||||
which the host interprets according to convention.
|
||||
|
||||
The result is **free-monadic IO** without extending the language runtime,
|
||||
adding AST nodes, or requiring a type system. The calculus stays pure; the
|
||||
host alternates between impure actions and pure evaluation.
|
||||
|
||||
---
|
||||
|
||||
## How it works: the two-phase boundary
|
||||
|
||||
### Phase 1 — Pure evaluation
|
||||
|
||||
A tricu program containing IO constructs is parsed, lambda-eliminated, and
|
||||
reduced exactly like any other program. `apply` never performs a side
|
||||
effect. The result is a first-class tree value.
|
||||
|
||||
### Phase 2 — Host execution
|
||||
|
||||
After pure evaluation completes, the host inspects the result. If it carries
|
||||
the `"tricuIO"` sentinel, the host strips the sentinel and enters a driver loop
|
||||
that walks the inner action tree, performing effects and calling back into
|
||||
the pure evaluator between each step.
|
||||
|
||||
This "ping-pong" between host and calculus is the only place impurity lives.
|
||||
|
||||
---
|
||||
|
||||
## The IO tree encoding
|
||||
|
||||
### Top-level sentinel: `ofString "tricuIO"`
|
||||
|
||||
The result of `main` must be a pair whose left element is the tree-encoded
|
||||
string `"tricuIO"` and whose right element is a versioned action:
|
||||
|
||||
```
|
||||
Fork
|
||||
├── ofString "tricuIO" -- sentinel (142 nodes)
|
||||
└── Fork
|
||||
├── ofNumber 1 -- ABI version
|
||||
└── action -- the actual IO program tree
|
||||
```
|
||||
|
||||
The `io` constructor in `lib/io.tri` bakes in the version:
|
||||
|
||||
```tri
|
||||
io = action : pair "tricuIO" (pair 1 action)
|
||||
```
|
||||
|
||||
The sentinel serves two purposes:
|
||||
|
||||
1. **Collision resistance.** A 142-node specific structure is effectively
|
||||
impossible to produce by accident in ordinary data.
|
||||
2. **Self-describing debuggability.** Evaluating `main` without the `--io`
|
||||
flag prints `{"tricuIO", [1, ...]}` literally, making the intent obvious.
|
||||
|
||||
The host checks: *is the root a `Fork` whose left child is equal to
|
||||
`ofString "tricuIO"` and whose right child is a `pair version action`?*
|
||||
If the version is unrecognized, the driver aborts with a clear error.
|
||||
Otherwise it enters IO mode on the action tree.
|
||||
|
||||
### Constructor payloads
|
||||
|
||||
The action tree uses tagged pairs. Tags are small integers (the existing
|
||||
tricu number encoding) because they are inspected on every loop iteration.
|
||||
The payload of each constructor is built with `pair` (i.e. `Fork`).
|
||||
|
||||
| Tag | Constructor | Payload shape | Continuation receives |
|
||||
|-----|-------------|---------------|----------------------|
|
||||
| `0` | `Pure result` | `result` | (terminal) |
|
||||
| `1` | `PutStr string k` | `pair string k` | `t` (unit) |
|
||||
| `2` | `GetLine k` | `k` | `String` |
|
||||
| `3` | `ReadFile path k` | `pair path k` | `Result IOError String` |
|
||||
| `4` | `WriteFile path contents k` | `pair path (pair contents k)` | `Result IOError Unit` |
|
||||
|
||||
Tag `0` (`Pure`) is the terminal node. All other constructors carry a
|
||||
continuation `k` — a tricu function (a tree) that the host applies to the
|
||||
operation's result to obtain the next action.
|
||||
|
||||
### Result encoding
|
||||
|
||||
File operations return explicit `Result` values using the same encoding as
|
||||
`lib/binary.tri`. Because there is no remaining stream, the `rest` field is
|
||||
always `t` (unit):
|
||||
|
||||
```tri
|
||||
ok = value : pair true (pair value t)
|
||||
err = code : pair false (pair code t)
|
||||
```
|
||||
|
||||
The host never throws raw exceptions. It translates OS failures (file not
|
||||
found, permission denied, etc.) into `err` trees with numeric codes and
|
||||
hands them to the continuation. The tricu program decides what to do with
|
||||
them.
|
||||
|
||||
### Visual example: `putStr "hi"`
|
||||
|
||||
After pure evaluation, `main = io (putStr "hi" (\_ : pure t))` becomes:
|
||||
|
||||
```
|
||||
Fork
|
||||
├── ofString "tricuIO"
|
||||
└── Fork
|
||||
├── ofNumber 1 -- ABI version
|
||||
└── Fork
|
||||
├── ofNumber 1 -- PutStr tag
|
||||
└── Fork -- pair "hi" k
|
||||
├── ofString "hi"
|
||||
│ └── Fork
|
||||
│ ├── ofNumber 104 -- 'h'
|
||||
│ └── Fork
|
||||
│ ├── ofNumber 105 -- 'i'
|
||||
│ └── Leaf
|
||||
└── k -- continuation function
|
||||
```
|
||||
|
||||
The continuation `k` is the SKI-combinator-lowered body of `(\_ : pure t)`.
|
||||
It is indistinguishable from ordinary data until the host `apply`s it to
|
||||
a value and evaluates the result.
|
||||
|
||||
---
|
||||
|
||||
## The host driver loop
|
||||
|
||||
```
|
||||
runIO(env, actionTree):
|
||||
case actionTree of
|
||||
|
||||
Fork Leaf result:
|
||||
-- Pure: done
|
||||
return result
|
||||
|
||||
Fork (Stem Leaf) (Fork str k):
|
||||
-- PutStr
|
||||
s = toString(str)
|
||||
putStr(s) -- impure
|
||||
next = evalASTSync(env, apply(k, t))
|
||||
return runIO(env, next)
|
||||
|
||||
Fork (Fork Leaf (Stem Leaf)) k:
|
||||
-- GetLine
|
||||
line = getLine() -- impure
|
||||
next = evalASTSync(env, apply(k, ofString(line)))
|
||||
return runIO(env, next)
|
||||
|
||||
Fork (Fork (Stem Leaf) Leaf) (Fork path k):
|
||||
-- ReadFile
|
||||
p = toString(path)
|
||||
checkHostReadPermission(p)
|
||||
result = hostReadFileAsResult(p)
|
||||
next = evalASTSync(env, apply(k, result))
|
||||
return runIO(env, next)
|
||||
|
||||
Fork (Fork (Stem Leaf) (Fork Leaf (Stem Leaf))) (Fork path (Fork contents k)):
|
||||
-- WriteFile
|
||||
p = toString(path)
|
||||
c = toString(contents)
|
||||
checkHostWritePermission(p)
|
||||
result = hostWriteFileAsResult(p, c)
|
||||
next = evalASTSync(env, apply(k, result))
|
||||
return runIO(env, next)
|
||||
```
|
||||
|
||||
Key properties:
|
||||
|
||||
- **No effects during `apply`.** The calculus stays pure.
|
||||
- **Fresh pure evaluation per step.** After each impure action, the host
|
||||
calls back into the ordinary evaluator to reduce the continuation.
|
||||
- **First-class continuations.** The continuation is a tree; it can be
|
||||
stored, passed around, or transformed by pure tricu code before the
|
||||
host ever sees it.
|
||||
- **Controlled failure.** File operations return `Result` trees; host
|
||||
exceptions are caught and converted into `err` values before they reach
|
||||
the calculus.
|
||||
|
||||
---
|
||||
|
||||
## Library conventions (`lib/io.tri`)
|
||||
|
||||
The IO constructors are ordinary tricu definitions. They are not primitives.
|
||||
|
||||
```tri
|
||||
io = action : pair "tricuIO" (pair 1 action)
|
||||
pure = x : pair 0 x
|
||||
putStr = s k : pair 1 (pair s k)
|
||||
getLine = k : pair 2 k
|
||||
readFile = p k : pair 3 (pair p k)
|
||||
writeFile = p c k : pair 4 (pair p (pair c k))
|
||||
```
|
||||
|
||||
### Why `readFile` and `writeFile` are sufficient
|
||||
|
||||
These two operations are powerful primitives on Unix-like systems. Standard
|
||||
input, output, environment variables, pipes, and special files in `/proc` or
|
||||
`/dev` are all reachable through the filesystem namespace. Additional
|
||||
constructors (`GetEnv`, `ExitWith`, `GetArgs`) are convenience wrappers
|
||||
that save the program from manually parsing `/proc/self/environ` or
|
||||
writing exit codes to special paths. The host is free to restrict which
|
||||
paths are accessible.
|
||||
|
||||
---
|
||||
|
||||
## Example program
|
||||
|
||||
```tri
|
||||
!import "io.tri" !Local
|
||||
|
||||
main = io (
|
||||
putStr "Name: " (\_ :
|
||||
getLine (\name :
|
||||
putStr "Hello, " (\_ :
|
||||
putStr name (\_ :
|
||||
pure t)))))
|
||||
```
|
||||
|
||||
The program is written in continuation-passing style. Each operation
|
||||
receives a continuation that receives the result and returns the next
|
||||
action. This matches the underlying tree encoding directly.
|
||||
|
||||
---
|
||||
|
||||
## Relationship to existing tricu features
|
||||
|
||||
IO is not a new kind of extension. It follows the same pattern already used
|
||||
for strings, integers, and lambda abstraction:
|
||||
|
||||
| Feature | Source syntax | AST representation | Pure tree | Host interpretation |
|
||||
|---------|---------------|-------------------|-----------|---------------------|
|
||||
| Strings | `"hello"` | `SStr "hello"` | `ofString "hello"` | Display with quotes |
|
||||
| Integers | `42` | `SInt 42` | `ofNumber 42` | Display as decimal |
|
||||
| Lambdas | `(x : x)` | `SLambda ["x"] (SVar "x")` | SKI combinators | N/A — eliminated |
|
||||
| IO | `io (...)` | `SApp` trees | Tagged sentinel pair | Enter driver loop |
|
||||
|
||||
The `T` type, `apply`, and the parser's core grammar require **no changes**.
|
||||
Only the host CLI and a new library file are needed.
|
||||
|
||||
---
|
||||
|
||||
## Implementation notes for host authors
|
||||
|
||||
### Required additions
|
||||
|
||||
1. **`lib/io.tri`** — constructor definitions.
|
||||
2. **Host sentinel check** — after evaluating `main`, test the root shape
|
||||
and ABI version.
|
||||
3. **`runIO` driver** — pattern-match on tags, alternate between effects and pure
|
||||
`evalASTSync` calls.
|
||||
4. **CLI integration** — an `--io` flag or `!run` REPL command to enable the driver.
|
||||
|
||||
### Host contract: strict validation
|
||||
|
||||
The IO driver must be a strict validator, not a permissive interpreter.
|
||||
|
||||
- Every tag must have exactly the expected payload shape. A tag `1` without
|
||||
a `pair string k` payload is a dynamic error.
|
||||
- String payloads must decode cleanly with `toString`; malformed character
|
||||
sequences must fail rather than silently truncate.
|
||||
- File paths must satisfy host policy (e.g. sandboxing, disallow lists,
|
||||
or capability restrictions). The host decides which paths are legal.
|
||||
- File operations must return `Result` trees. Host exceptions are caught
|
||||
and converted to `err` values before reaching the calculus.
|
||||
- Continuations must reduce to another valid action tree or `Pure`. If the
|
||||
pure evaluator returns an unrecognized shape, the driver aborts with a
|
||||
clear dynamic error rather than guessing.
|
||||
- Unrecognized ABI versions must be rejected immediately.
|
||||
|
||||
These checks are runtime-only. The calculus does not enforce them; the host
|
||||
does.
|
||||
|
||||
### Recommended restrictions
|
||||
|
||||
- Do **not** modify `apply` or `evalASTSync` to perform effects. Keep the
|
||||
calculus pure.
|
||||
- Do **not** add new `TricuAST` constructors for IO. Use ordinary `SApp` trees.
|
||||
- Tag numbers are host convention; document them if you extend the set.
|
||||
- The `"tricuIO"` sentinel string and the ABI version are part of the
|
||||
convention. Changing either breaks compatibility.
|
||||
|
||||
### Extending the IO vocabulary
|
||||
|
||||
New constructors receive new tags, documented payload shapes, and explicit
|
||||
result conventions. Existing programs that do not use the new tag are
|
||||
unaffected. If a breaking change to payload shapes is ever needed, bump
|
||||
the ABI version and teach the host to recognize both.
|
||||
|
||||
---
|
||||
|
||||
## Comparison to Haskell's `IO`
|
||||
|
||||
| Property | Haskell | tricu |
|
||||
|----------|---------|-------|
|
||||
| Purity guarantee | Type system (`IO` is a distinct type) | Host convention (sentinel check) |
|
||||
| Sequencing shape | `RealWorld#` token threaded by RTS | Host driver loop calls pure evaluator between steps |
|
||||
| Linearity | Enforced statically by compiler | Enforced dynamically by host loop (tree walked once) |
|
||||
| Inspectability | `IO a` is opaque; cannot pattern-match | IO tree is first-class data; can be constructed, deconstructed, and transformed in pure tricu code |
|
||||
| Entry point | `main :: IO ()` required by compiler | `main` checked for sentinel when `--io` is passed |
|
||||
|
||||
Haskell's type system provides static guarantees. tricu provides a
|
||||
Haskell-like sequencing shape that is dynamically enforced by host
|
||||
interpretation. Incorrectly-shaped IO trees are caught at runtime, not
|
||||
compile time.
|
||||
|
||||
---
|
||||
|
||||
## Future-proofing
|
||||
|
||||
The ABI is designed so that a future type system can describe the same
|
||||
boundary statically without changing the runtime encoding.
|
||||
|
||||
Conceptually, the constructors have stable shapes:
|
||||
|
||||
```text
|
||||
Pure : a -> IO a
|
||||
PutStr : String -> (Unit -> IO a) -> IO a
|
||||
GetLine : (String -> IO a) -> IO a
|
||||
ReadFile : Path -> (Result IOError String -> IO a) -> IO a
|
||||
WriteFile : Path -> String -> (Result IOError Unit -> IO a) -> IO a
|
||||
```
|
||||
|
||||
Even though tricu cannot check these types today, the host preserves them:
|
||||
- Every constructor has a predictable tag and documented payload layout.
|
||||
- Every continuation receives exactly one well-defined result value.
|
||||
- File operations return `Result` trees instead of throwing host exceptions.
|
||||
- The ABI version marker leaves room for protocol evolution.
|
||||
|
||||
Capabilities and sandboxing are host policy, not tree shape. The CLI should
|
||||
restrict paths with flags such as `--allow-read` and `--allow-write`. A
|
||||
future typed system may add unforgeable capability types; today's host
|
||||
enforces restrictions dynamically.
|
||||
|
||||
---
|
||||
|
||||
## Summary
|
||||
|
||||
tricu programs construct pure descriptions of effects. The host executes one
|
||||
submitted description according to policy. IO is not part of the calculus;
|
||||
it is a **host convention** layered on top, using the same "host introduces
|
||||
structured values" mechanism already employed for strings and numbers. The
|
||||
result is a free-monadic interaction tree that any host can execute, any
|
||||
program can manipulate as data, and any Merkle DAG can store. Sequencing
|
||||
and linearity are enforced dynamically by the host, not statically by the
|
||||
language.
|
||||
Reference in New Issue
Block a user