1ML with special effects: F-ing generativity polymorphism

Abstract

We take another look at 1ML, a language in the ML tradition, but with core and modules merged into one unified language, rendering all modules first-class values. 1ML already comes with a simple form of effect system that distinguishes pure from impure computations. Now we enrich it with effect polymorphism: by introducing effect declarations and, more interestingly, abstract effect specifications, effects can be parameterised over, and treated as abstract or concrete in the type system, very much like types themselves. Because type generativity in 1ML is controlled by (im)purity effects, this yields a somewhat exotic novel notion of generativity polymorphism- that is, a given functor can be asked to behave as either “generative” or “applicative”. And this time, we even get to define an interesting (poly)monad for that!