v0.0.11: proper pure IO

This commit is contained in:
2025-09-12 14:22:57 +02:00
parent 4fba995390
commit c607dd5277

62
spec.md
View File

@@ -376,22 +376,67 @@ myHeader with header:text: "new meta:header:text value"
## Pure IO ## Pure IO
the `IO[t]` type contains IO "plans" which will be executed by the runtime, if they are returned by the main function.
```
def main() -> IO[Unit] {
print("hey") # warning: result (of type IO[Unit]) was ignored. expression can be removed
print("hello")
}
# this will only print "hello"
```
To make the above example print both "hey" and "hello", we need to chain the two IO types:
```
def main() -> IO[Unit] {
await _ = print("hey")
await print("hello")
}
# or just remove the _
def main() -> IO[Unit] {
await print("hey")
await print("hello")
}
# if you don't put in the second await:
def main() -> IO[Unit] {
await print("hey")
print("hello")
# error: expected IO[Unit], got IO[IO[Unit]]; did you forget an `await`?
}
```
await is kinda weird. here is the syntax:
```
# ( await x: a = ( expr1::IO[a] ) await (expr2::IO[b]) ) :: IO[b]
expr |= 'await', (identifier, '='), expr, 'await', expr
# ( await x: a = ( expr1::IO[a] ) ( expr2::b ) ) :: IO[b]
expr |= 'await', (identifier, '='), expr, expr
# ( await (expr1::a) ) :: a
expr |= 'await', expr
```
## Pure IO implementation
Something like this is done in the stdlib: Something like this is done in the stdlib:
``` ```
extensible union IO.Plan[r] extensible union IO.Plan[r]
type IO[t] = 'Just {value: t} type IO[t] = 'Just {value: t}
| 'More template r, f: {plan: IO.Plan[r], then: r -> IO[f], finally: f -> t} | 'Map template r: {of: IO[r], map: r -> IO[t]}
| 'More template r: {plan: IO.Plan[r], then: r -> IO[t]}
def [a,b] `await a (a->b)`(io: IO[a], then: a -> b) -> IO[b] { def [a,b] `await a (a->b)`(io: IO[a], then: a -> b) -> IO[b] {
match io { 'Map {of: io, map: r -> 'Just {value: then(r)}}
'Just {value} -> 'Just {value: then(value)}, }
'More &a {finally,...} -> a with finally: r -> then(finally(r))
} def [a,b] `await a (a->await b)`(io: IO[a], then: a -> IO[b]) -> IO[b] {
'Map {of: io, map: r -> then(r)}
} }
# in stdio: # in stdio:
extend IO.Plan[Uint8] with 'stdio.ReadByte {stream: Int32} extend IO.Plan[Uint8] with 'stdio.ReadByte {stream: Int32}
def stdio.getchar : IO[Uint8] = 'More {plan: 'stdio.ReadByte {stream: 0}, then: by -> 'Just by[0], finally: x->x} def stdio.getchar : IO[Uint8] = 'More {plan: 'stdio.ReadByte {stream: 0}, then: by -> 'Just by[0]}
def main() -> IO[Unit] def main() -> IO[Unit]
``` ```
@@ -401,10 +446,11 @@ the runtime does something like this:
def [a] RUNTIME_EVAL(io: IO[a]) -> a { def [a] RUNTIME_EVAL(io: IO[a]) -> a {
match io { match io {
'Just {value} -> value 'Just {value} -> value
'More {plan, then, finally} -> finally(RUNTIME_EVAL(then(match plan { 'Map {of, map} -> RUNTIME_EVAL(map(RUNTIME_EVAL(of)))
'More {plan, then, finally} -> RUNTIME_EVAL(then(match plan {
'ReadStream {stream} -> 'ReadStreamIOResult {data: impure perform the io here lol} 'ReadStream {stream} -> 'ReadStreamIOResult {data: impure perform the io here lol}
_ -> impure error here "this runtime doesn't support this kind of IO" or sth _ -> impure error here "this runtime doesn't support this kind of IO" or sth
}))) }))
} }
} }