|
|
|
|
|
|
by ux266478
13 days ago
|
|
|
I'm actually not a fan of Idris' implementation of the IO monad, it really should have been a free monad with a cofree comonad so you can enforce invariants against the world without a bunch of extra machinery. It seems kind of important for a dependent type system. I quite like Mercury's non-monadic linear IO + determinism semantics. You can subtype the world with insts and unify against the world-state pretty easily. |
|
|