Some further info. A follow-up paper 1ML with Special Effects [1] extends the original 1ML type system with effects polymorphism (i.e. that higher order functi

Some further info. A follow-up paper 1ML with Special Effects [1] extends the original 1ML type system with effects polymorphism (i.e. that higher order functions such as ‘map’ can either be pure/applicative or impure/generative), but IMO at a huge loss of simplicity of the original paper - essentially you need a limited implementation of type classes! An important (in my opinion) extension of 1ML would be value tracking, which was implemented for modules in the earlier F-ing Modules paper, and would solve some of the remaining issues with ML module system. I tried doing that (only implementation, not theory, and without type inference), but it’s... hard (and I’m not sure it can be done keeping the simplicity of 1ML). [1] https://people.mpi-sws.org/~rossberg/1ml/1ml-effects.pdf https://people.mpi-sws.org/~rossberg/1ml/1ml-effects.pdf