Three Dollar Quill

Okay, let's see if I can take some notes quickly. I'm working from the algebraic effects technical report, as well as the effect polymorphism and extended writeups of 1ML.

Both of these three papers have a mapping from higher-level types to lower-level types. The mapping I will end up with will draw a lot from 1ML, but will draw from alebraic effects, in that effects beyond the basics will have additional effects on the return types of functions. Basically, I think I need to figure out how to combine the two monads that the different papers are talking about, which is annoying in general, but hopefully doing it in a sort of specific context like this will make things not too bad.

Before anything else (and with not much after it, because I spaced out and it's super late), let's see if I can figure out what the signature of a map function looks like.

map : (a : type) ->p (b : type) ->p (m : effect) ->p ((a) ->m b) -> (list a) ->m (list b) Or something like that.

Now, here's what I know very offhand:

• 1ML syntax manipulations should handle a lot of this even before I get algebraic effects in the mix, and they shouldn't make too much of a difference to the implementation.
• I definitely want to make sure that the type and effect arguments can generally be inferred.
• My big concern is how to handle "oh yeah, sometimes the function type is wrapped in existential types, sometimes it isn't" from 1ML. I don't see how to do that, unless actually I'm wrapping the entire function type in a bunch of alternatives.
• Regardless, the play looks to be "how do I integrate 'wrap this type in a monad' with 1ML's weird bespoke polymorphism?" Part of that question is "1ML semantic types have a lot of pieces; at what level does the monad wrapping go?"

Anyway, I'll try to come up with an answer to those at a not-messed-up time of day, later, since it's way too late to do it now.

Good night.