Three Dollar Quill

Okay, I'm over-engineering my efforts to tweak the 1ML elaboration, so let's put that down for a bit. Let's take a look at algebraic effects in a non-ML context.

I'm right now working from Appendix C of Generalized Evidence Passing for Effect Handlers. This presents an elaboration to some form of System F, and hey, I've implemented some form of System F! Probably not the same form, but I'm having some trouble parsing out the fine details, currently.

In any case, let's go through the rules and see how much I'll mess with them.

• var synthesizes the type
• abs is on the one hand straightforward (check the type, bind the variable, check the body against the result type and effect to elaborate out the body, presumably wrap the result in an ascription that contains the transformed function type, which requires the same junk that has me stuck on 1ML, transforming a function type to reflect the effect of the effect), but on the other hand, reveals some differences with my own "some form of System F". Specifically, the expression/value distinction here is between introduction forms and elimination forms, with a "value" expression to implicitly bridge between them. My gut reaction is to treat computations the way this appendix treats "expressiona", and basically have introduction computations unify their effect with the empty row.
• val would correspond to the Return node under this system; possibly the other introductory computations could be wrapped in a thunk?
• tabs... the type-level distinction will have to be collapsed in some way when it comes to integrating this with 1ML; I'm not going to think about this too hard, but I am going to think about it. Things of note: apparently labels are the equivalent of a large type in 1ML, and also this translation barely does anything, which I'm going to hope is a good sign.
• app has some confusing bits, but the key thing to keep in mind is that the elaborated code has a bunch of monadic binds, which are going to require that I support enums/unions/whatever.
• tapp looks innocent until the elaboration, which, let's see, monadic bind, monadic translation, probably fine.
• perform looks like it needs to synthesize, and it needs op to synthesize, I think.
• ops has an unmatched brace in the elaboration that I think goes somewhere near the beginning (or maybe it should just be deleted). My gut impression looking at this is that it should be checking.
• handler might be synthesizing.
• prompt needs to synthesize from h, then has enough information to check e and synthesize overall.
• yieldb has to synthesize from f, and then it either checks overall and k, or it does all synthesis and some unification; let's see if the former can work.
• under, I'm not sure what to think; it's capable of synthesizing almost everything, but that's a load-bearing "almost". No matter what it does, there's going to be some kind of unification.

No telling whether I'll end up making use of any of these notes. I'm going to try to step away, and then investigate whether the monadic translation from page 22 of the technical report can be made compatible with 1ML semantic types. Right now, I really need to stop looking at screens.

Good night.