Note that in the original papers the stacking is limited by "Row", i.e. you cannot stack M A0 () with M A1 () (higher-ordered free monads). The implementation in Idris2 doesn't have this limitation. Maybe it is a limitation from the Hindley-Miller type system.
Hello, I didn't see algebraic effects mentioned in the Dao of FP, so here's some information about it.
If you have
M0 ()andM1 (), you can stack them and getUnion [M0, M1] ()A programming language using this trick to make reasoning about effects easier: https://koka-lang.github.io/ References: https://koka-lang.github.io/koka/doc/book.html#sec-implementation Implementation in Idris2: https://github.com/locriacyber/idris2-eff
Note that in the original papers the stacking is limited by "Row", i.e. you cannot stack
M A0 ()withM A1 ()(higher-ordered free monads). The implementation in Idris2 doesn't have this limitation. Maybe it is a limitation from the Hindley-Miller type system.