Three Dollar Quill

All right, I've read up on effect types, and as I side, I'm interested in the theoretical implications of taking the paper's construction of them over a typed lambda calculus, and instead doing that above 1ML. I think the specific interaction I'm interested in is, what happens if I perform an effect in a function that returns a value of type type. But probably the more practical focus is, can I have different "top-level handlers" in different execution contexts, and then structure function calls something like [all type arguments] -> [evidence vector that can be evaluated at compile time] -> [actual arguments] -> [evidence vector that can be evaluated at run time] -> [return type]?

However, I don't want to rush into anything, so I'm back to reading up on refinement types. I'm not going too quickly, since I think I'm still feeling some of the effects of last night. I'm going to wrap this post up now.

Good night.