A few weeks ago, I showed a very simple model for constructing and storing typed combinators incrementally. By incremental, I meant that type-checking was a sequential and iterative process: instead of giving it a whole term, type-checked at once (the usual, batch approach), you could split it up into pieces and commit each of them individually. Each commit would give you a unique identifier for the piece of term you just provided, and if the user bothers to write down these names, he can then elaborate new terms on top of them, possibly in a non-linear fashion. That way, we can model bottom-up term construction, and incrementally modify a term.
We noted also some defects to this approach, two of which we are going to address today: one is the absence of top-down construction (a very common way of building terms incrementally), the other is the burden of remembering names for successive versions. The interesting part is that we are going to simulate them inside our model, taking advantage of the extensibility of the signature.