4 ms·
I wonder if a type system could track nondeterminism and prevent it. E.g. you couldn't just loop over a set, you'd have to order it, or apply a commutative oper
by tracnar 4y ago
I wonder if a type system could track nondeterminism and prevent it. E.g. you couldn't just loop over a set, you'd have to order it, or apply a commutative operation. It would fit well into concurrency too, where nondeterminism is easily introduced.
I'm sure there are languages which do this, I seem to recall seeing it in Mercury
- phlip9 4y agoLanguages with first class effects, like koka[1], require you to declare up-front what side effects (sample randomness, do I/O, abort, etc...) your function might cause. Then from another outer function, you can't call the effectful function unless the outer function also declares those same side-effects (or you provide handlers for them). This way you can easily isolate non-determinism and I/O to the top-level part of your program, while keeping the interior business logic pure. The "first-class effects" part is what lets you easily compose effects and inject custom handlers. Ideally in a way that's more ergonomic than juggling with Monad type system Jenga. [1]: https://koka-lang.github.io/koka/doc/index.html https://koka-lang.github.io/koka/doc/index.html