Three Dollar Quill

Okay, let's kind of start over with my ideas about semantic types.

For now, I divide them into pure values and computations, and impure values and computations. Pure values are the simplest representation of the type, and computation types are simply returning the corresponding value type. This means that base values are now directly the pure type, and abstracted or function values are thunks. For now, impure values are simply pure values wrapped in a thunk-return. We consider semantic types in general, separately from semantic types with purity annotations, even though general semantic types and pure values have the same representation.

The contexts where these different representations matter are that variables are bound with purity annotations, and the result type of functions is a computation with a purity annotation. Hopefully, it is then possible to ensure that all expressions infer or check annotated types.

Looking over the expressions to be synthesized, I now suspect the correct interpretation is that expressions are typed with annotated values types, but the synthesized expressions are computations corresponding to returning a value of that type.

This all seems reasonable. Past experience tells me that now is the time to step back and let this percolate for a bit. If it still seems sensible after that, I'll start filling in notes. Until then, I'm going to read up on refinement types to see if my ideas about how to incorporate them into purity annotations make sense.

For the immediate term, though, I'm going to try wrapping up this entry before it's suddenly midnight.

Good night.