Idris 2 has some really interesting stuff with linear types. IO is implemented using a linear "world" token. Every I/O operation consumes the current state of t

Idris 2 has some really interesting stuff with linear types. IO is implemented using a linear "world" token. Every I/O operation consumes the current state of the world and returns a new state of the world. Each state of the world must be used exactly once. And the IO monad ends up just being syntactic sugar around this. See https://github.com/stefan-hoeck/idris2-tutorial/blob/main/src/Tutorial/IO.md#how-io-is-implemented https://github.com/stefan-hoeck/idris2-tutorial/blob/main/sr...