Coding 2025-01-10
All right, I finished some reading on types, and now I've got more reading to do. To be clear, it is basically certain that I'm going to have to revisit this reading, almost from the beginning, but I do feel like I got some key insights from it. However, at this point, I think I really need to focus on two things: how to implement an effect system, and getting a feel for 1ML.
This is because... let me see if I can get this to make sense. 1ML attempts to unify the syntax for type-level and term-level functions. I think. It appears to me that doing so in the context of an effect system would give an implementation of implicit function arguments; those would be from effects that are handled at compile time. The failure mode for a typing algorithm is to fail to terminate. An effect system can (and in Koka, does) model the possibility of a particular computation failing to terminate.
With all of that in mind, the overall direction I'm trying to go seems like it has three possible endpoints, and I'm not sure which to expect:
- It is possible to disallow non-termination at compile time, but still have expressive constructs, provided a non-termination proof is provided.
- I somehow mess things up so badly that literally every compile-time function that does anything remotely interesting needs to be marked as potentially non-terminating.
- It turns out that potentially non-terminating code is somehow not fundamentally any more interesting.
In any case, I would very much like to see how getting an effect system to work with 1ML (if that's actually possible the way I'm imagining it) stacks up against COCHIS.
Okay, that's all for now. Time to wind down.
Good night.