Three Dollar Quill

Okay, I'm letting stuff for the conlanging code kind of just percolate.

Let's take stock of Impliciula. There's some functionality in here that got kind of messy, and it's clear that I didn't think through how it should be used.

The basic idea is, there are different extensions to the simply-typed lambda calculus, and I managed to write code that can represent different extensions in a typed fashion. So, like, it's possible to have basic simply-typed lambda calculus, system F, system F with existential types, etc. Each node is only implemented once, and the specific combination of allowable nodes is handled in a module for the specific extension of the lambda calculus. The problem I have right now is that I don't have a clear picture of what should be allowed by default. Because the current state is so disordered, I'm going to try to lay out how things should work.

• The base STLC is CBPV with bidirectional typing. This means that it needs variables, thunks, forces, returns, sequencing, abstractions, applications, and ascriptions. Furthermore, higher-level features require type variables and the kind of proper types, as well, and typing requires several "failed" nodes, which are in kind of a confusing place.
• In order to actually compute an externally useful value, basic scalar types are needed, at minimum.
• System F extends with type abstractions and type applications.
• Additionally, packing and unpacking.
• In order make use of packed values, record types and projections are needed.
• Lastly, type operators and operator applications are needed for System Fω.

The idea of breaking up the nodes into distinct features, suggests a means of streamlining the current implementation: instead of the current approach of enumerating all (most) nodes of interest, have a single type parameter that can be unioned with a marker type representing a constellation of related features. This should simplify things; I'll need to make sure it doesn't somehow simplify "too much".

With this level of simplification, it could make sense to introduce more nuance into the base types. Make a given syntax tree module specify a combination of features and base types. Then the default can be CBPV and bidirectional typing, plus support for higher-level features, and the extensions can be base types, universal types, existential types, type operators, and record types. The resulting syntax tree types should generally be parametric over base types, since they don't do anything "interesting" to tree structure. Therefore, it could be clean to make this all a two-variable system, with one variable for node types, and one variable for base types.

As I think about this, it also occurs to me that so many imports would be simplified if I were to put together some kind of subclassable builder class, like I've considered before.

I think this is a promising direction to take the code, if a little obnoxious to do all of the updates. I just need to give things a little more thought to make sure they all fit together. (The current source of annoyance for me is, if typing fails, there could very well be a failed node somewhere in the result, but if it succeeds, then there shouldn't be a failed node. Do I need to thread a result type through all of type inference to get the results I want? I want the answer to be "no"... All of this said, nothing in the current types stops inference from returning garbage, so on the one hand, it could be defensible to do the updates I know how to do now, and the rest later, but on the other hand, I want to make sure I don't accidentally impede those later updates. I've got to think...)

Not going to get any further on this tonight, need to wind down.

Good night.