Three Dollar Quill

All right, it's really late, but let's see if I can work something out. I'm right now looking into the coercion between the pure and impure functions from bool to bool. For various reasons, I believe the types of these functions in System Fω would be FuncType(ThunkType(ReturnType(bool_)), ReturnType(bool_)) and FuncType(ThunkType(ReturnType(bool_)), ReturnType(ThunkType(ReturnType(bool_)))), respectively.

Let's start by checking pure to pure, just to make sure we actually get a reasonable identity function.

Now, the coercion function in this case probably has type FuncType(ThunkType(FuncType(ThunkType(ReturnType(bool_)), ReturnType(bool_))), ReturnType(ThunkType(FuncType(ThunkType(ReturnType(bool_)), ReturnType(bool_))))), assuming I didn't get distracted while typing all that. The outermost layer of wrapping in the result type may be unnecessary, but I'm not currently sure how to evaluate that.

Anyway, to inhabit this, we need an Abstraction(x, Return(Thunk(Abstraction(y, ...)))) I'm not getting the inside of that right in my head. I'll just note that both of the internal coercion functions have type FuncType(ThunkType(ReturnType(bool_)), ReturnType(ThunkType(ReturnType(bool_))))

I'll also note that the outermost layer of wrapping does appear necessary, and it should go around the type abstractions, if any. Anyway, let's see if I can sketch out what has to happen here. The coercion function can apply directly to y, so then we have a return-thunk-return, which is sequenced into x, producing a return, which seems like it will cause problems.

I'm not going to look into it right now, but perhaps the coercion functions have to be pure identities rather than impure identities. That doesn't quite feel right, because then the function arguments all kind of run together. If the impure identity works, then we need to first thunk the entire computation up through sequencing into x, pass that to the coercion function, and then... sequence it into a force? That's either the obvious solution, or it won't work at all. I'll try to figure out which in the morning.

Either way, if this all works, then the pure to impure version would need to wrap the whole thing in a return-thunk, and the impure to impure... we'll see.

Anyway, I spent long enough on this, time to get to bed.

Good night.