CPS IO -> Async Interaction Tree Effect Runtime

I'm deeply satisfied to be building an interaction tree runtime where
the interaction trees are themselves computed via and represented by
trees. It's trees all the way down.
This commit is contained in:
2026-05-13 11:02:37 -05:00
parent 983a0cc5a7
commit 8f7684a1bb
6 changed files with 1965 additions and 117 deletions

View File

@@ -3,80 +3,82 @@
!import "conversions.tri" !Local
-- IO constructors for host-interpreted interaction trees.
-- See docs/io-in-tricu.md for the full protocol.
-- Free-monad style: Bind is the single sequencing mechanism.
version = 1
io = action : pair "tricuIO" (pair version 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))
pure = x : pair 0 x
bind = action k : pair 1 (pair action k)
putStr = s : pair 10 s
getLine = pair 11 t
readFile = p : pair 20 p
writeFile = p c : pair 21 (pair p c)
ask = pair 30 t
local = f action : pair 31 (pair f action)
get = pair 40 t
put = s : pair 41 s
fork = action : pair 60 action
await = handle : pair 61 handle
yield = pair 62 t
sleep = ms : pair 63 ms
-- ---------------------------------------------------------------------------
-- CPS sequencing helpers
-- Generic sequencing combinators
-- ---------------------------------------------------------------------------
-- Print a string and finish successfully.
print = s : putStr s (_ : pure t)
thenIO = a b : bind a (_ : b)
mapIO = action f : bind action (x : pure (f x))
-- Print a string plus newline and finish successfully.
printLn = s : putStr (append s "\n") (_ : pure t)
-- ---------------------------------------------------------------------------
-- Convenience helpers
-- ---------------------------------------------------------------------------
-- CPS print with newline.
putStrLn = s k : putStr (append s "\n") k
-- Sequence after putStr, ignoring Unit.
afterPutStr = s next : putStr s (_ : next)
-- Sequence after putStrLn, ignoring Unit.
afterPutStrLn = s next : putStr (append s "\n") (_ : next)
print = s : bind (putStr s) (_ : pure t)
putStrLn = s : bind (putStr (append s "\n")) (_ : pure t)
-- ---------------------------------------------------------------------------
-- Result-aware file helpers
-- ---------------------------------------------------------------------------
-- Read a file, forcing the caller to handle both success and error.
onReadFile = (path errCase okCase :
readFile path (result :
bind (readFile path) (result :
matchResult errCase okCase result))
-- Write a file, forcing the caller to handle both success and error.
onWriteFile = (path contents errCase okCase :
writeFile path contents (result :
bind (writeFile path contents) (result :
matchResult errCase okCase result))
-- ---------------------------------------------------------------------------
-- Convenience helpers for the common cases
-- ---------------------------------------------------------------------------
-- Read a file; on error print a message and finish.
readFileOrPrintError = (path okCase :
onReadFile path
(err rest :
putStrLn "Read failed" (_ :
pure t))
(err rest : putStrLn "Read failed")
okCase)
-- Write a file; on error print a message and finish.
writeFileOrPrintError = (path contents okCase :
onWriteFile path contents
(err rest :
putStrLn "Write failed" (_ :
pure t))
(err rest : putStrLn "Write failed")
okCase)
-- Copy src to dst, then continue with k on success.
copyFile = (src dst k :
onReadFile src
(err rest :
putStrLn "Read failed" (_ :
pure t))
(contents rest :
onWriteFile dst contents
(err rest :
putStrLn "Write failed" (_ :
pure t))
(ok rest :
k t)))
copyFile = (src dst :
bind (readFile src)
(result :
matchResult
(err rest : putStrLn "Read failed")
(contents rest :
bind (writeFile dst contents)
(wr :
matchResult
(err rest : putStrLn "Write failed")
(ok rest : pure t)
wr))
result))