Three Dollar Quill

I didn't have as much focus as I would have liked, but I'm making a little progress thinking about what I'm going to do for semantic types.

The change I'm thinking about right now is extending semantic types to handle algebraic effects. It looks like I just need to say "okay, in the result type of functions, in addition to indicating the purity, there's going to be another function that maps an evidence vector to a 'control monad'". Now, the control monad is going to require an amazing amount of effort to parse, it looks like, but it does appear parseable.

Let's think a little about the refinement types stuff. I haven't properly read over much of that paper, but I see that it will probably take some changes; constructing the constraints involves running backwards through the construction of the environment. Not particularly challenging to support, but it's definitely going to be an implementation change. Furthermore, some modifications will need to be made to subtyping. All of these papers want to do different things to functions, and right now I can only hope that these things can be made compatible. Since 1ML does a bunch of stuff with existential types already, I could consider using them for synthesis in the context of applications, but that's probably not a good idea in the face of 1ML's small/large types distinction.

Anyway, it's late again. I'll see how much focus I can give this tomorrow.

Good night.