So this is something I've been thinking about with my effect system which in the process of being born (preliminary codegen & typing works). Right now, I implement it as stack-walking but one of my goals is to monomorphise *everything* (no runtime HKTs) a consequence of... (1/n)
Conversation
...this is that generic effects (i.e: where generic parameters aren't specified in an effect type, such as async/await) codegen doesn't really compose and can only be done at a best-effort level. I am very unhappy with this, so I've been thinking of changing effect types to (2/n)
1
1
be more akin to impl Trait / existential types, thereby statically promising that monomorphisation (& also inlining) is possible. I need to do a lot more thinking about this though because I think it's going to have far-reaching consequences for effects in general. Any thoughts?
1
Hmm not sure. Pretty interested in what Effekt does with this stuff - I think they compile to a representation where handlers are injected as parameters?
2
I think a problem with this is that, again, monomorphisation can only occur on a best-effort basis (unless these 'parameters' are generic, as in Rust's Fn traits)
1
What do you mean by best effort?
2
As in: only when the compiler can infer that it's permitted to do so. I don't think this generalises very well because the compiler needs to keep track of the entire call stack, even in the presence of callbacks and conditionals and other weirdness like like that
2
Is this like… binding time analysis? Sorry not really great at back-end stuff. If so, have you looked at stuff like staging? There are a few approaches you can do, for this, but it amounts to being able to statically analyse when code is partially evaluated.
1
I'll do some reading, although from a cursory look I don't *think* staging really addresses this (at least, not in the general case).
2
Also there's one of those overwhelming bibliographies of stuff on MetaML, MetaOCaml, and typed template Haskell, etc. here: github.com/metaocaml/meta. This is also a cool recent thing which is based on 2LTT: github.com/AndrasKovacs/s
1
Not sure if folks have yet tackled combining this stuff with effect systems yet though. Could be interesting though. My hope is that you could somehow of tell the compiler at one point to generate code for a bunch of composed handlers.
And yeah, of course you'd get an error if you can't 'bake' those handlers into a statically known thing. This is kind of where I'd imagine the staging would come in, but I dunno.