Coding 2026-03-02

Tags:
By Max Woerner Chase

Okay, so. I guess what I realized while I was asleep is, I appear to have made a bad assumption about how semantic types work, which was making everything more complicated than it needed to be. Let's start over and see if I can get to a better place.

Where I believe I went wrong was in assuming that the elaboration rules were outputting complete programs. This led to a profusion of thunk-return wrapping, and more importantly, made it impossible to express certain function types in my fiddly System Fω variant. So, let's instead assume that they're outputting values, and the whole program is implicitly wrapped in a top-level Return.

This means that base types now just correspond directly to themselves, and many elaboration rules are now wrapped in a thunk. Anyway, let's try reworking the stuff I dashed out last night.

The pure identity is now of type FuncType(bool_, ReturnType(bool_)). The impure identity is now of type FuncType(bool_, ReturnType(ThunkType(ReturnType(bool_))))

The inner coercion functions f1 and f2 are now of identical type to the pure identity, and the outer coercions are now of type:

Let's try expressing this stuff in a code block, so I can have nice things like... indentation. Now, I've got to remember the rules. First, f1 applies to y. Then x applies to the result of that. Then f2 applies to the result of that. Then the purity coercion is applied. Maybe those last two go in the other order?

# General code:
Application(f1, y)  # ReturnType(bool_)
Sequence(Application(f1, y), y2, Application(Force(x), y2))  # Depends on purity of x

# Sorry to ramble in the middle of the code block, but this is really the crux of it all.
# The type of that sequence is going to be the same as the result type of the inner...
# I've been calling them identities, but they could be inverters or constants.
# Anyway, once we have either ReturnType(bool_) or ReturnType(ThunkType(ReturnType(bool_)))
# we need to apply f2, which, remember, is always of type FuncType(bool_, ReturnType(bool_))
# In the pure case, we can (probably) sequence the result directly through f2,
# giving us a ReturnType(bool_), which can be left alone,
# or sequenced through Abstraction(z, Return(Thunk(Return(z)))).
# (Or the whole thing could be wrapped in a Return(Thunk(...))?)
# Alternatively, we could be in the impure case, which means we have a
# ReturnType(ThunkType(ReturnType(bool_))), and we want to apply f2 in a way that gets us another
# ReturnType(ThunkType(ReturnType(bool_))).
# This will look like
# Sequence(x_res, v1, Sequence(Force(v1), v2, Application(f2, v2))) but with return-thunk wrapping... somewhere.

# pure-pure
Ascription(
    Abstraction(
        x,
        Return(Thunk(
            Abstraction(
                y,
                Sequence(
                    Sequence(
                        Application(f1, y),
                        y2,
                        Application(Force(x), y2),
                    ),
                    v1,
                    Application(f2, v1),
                ),
            )
        )),
    ),
    FuncType(
        ThunkType(FuncType(bool_, ReturnType(bool_))),
        ReturnType(ThunkType(
            FuncType(
                bool_,
                ReturnType(bool_),
            )
        )),
    )
)

# Looking over this, I believe the core of the purity coercion has to focus on the line
# Application(f2, v1)
# In the pure-impure case, this can be Return(Thunk(Application(f2, v1))).
# In the impure-impure case, this can be Sequence(Force(v1), v2, Return(Thunk(Application(f2, v2))))
# I think.

Okay, I've got a sketch of the concrete implementation (if we ignore type variables), but I think it would genuinely help at this point to think about monads. I now kind of see that the idea is, I think, to treat pure values as regular things, and impure values as a basic monad. To bring a value into the monad, it gets wrapped in a Thunk(Return(...))), and if f is a function of the appropriate type, then the binding operation on x looks like Abstraction(x, Abstraction(f, Sequence(Force(x), x2, Return(Thunk(Application(f, x2)))))), maybe.

What I'm getting now is that the particular monad implementation is, well, it's still important, but what I really need is a framework for working with arbitrary monads.

Now, when you get right down to it, the identity operator for proper types is technically a monad.

Anyway, I'm not sure if I'm looking at this stuff right. Like, for sure, pure-impure does a unit, and impure-impure does bind and unit. But ultimately, what is happening is that we have two monads, and three maps between them. So, given that, I want to step back from this again, and figure out how these monad types are supposed to interact when there's more going on.

My gut feeling is that, if I'm to get effects working at compile time, then the "purity" annotation has to go around everything else. (That's a load-bearing "if".)

Anyway, that's about enough for tonight. I'm going to wrap up early and ponder this stuff some more.

Good night.