some ideas for cleaning up the treatment of syntax

[jonsterling]

This branch experiments with some ideas to clean up the treatment of syntax. The main idea is:

1. Introduce a notion of Signature which is essentially the signature endofunctor of a second-order language
2. Define the substitution tensor: this is that left-kan-extension looking thing, which is like "heterogeneous closure"
3. Introduce sigma-monoids (under the name Model), which are algebras for the signature endofunctor equipped with a monoid action for the substitution tensor
4. Give a few examples of models: the initial model, and the "disected" model (which is the one that is used in the proof state)

Cool thing about this is that we can generically generate a model of a signature which is hash-consed, and implement its substitution action with memoization; this needs to be done only once, and can be applied to all signatures.

[jonsterling]

@freebroccolo Does this stuff look plausible? If so I'd like to rearchitect things around it generically, in light of #16.

[ghost]

@jonsterling Yeah, this sounds to me like a pretty nice idea. I think it's certainly worth trying.

[jonsterling]

@freebroccolo I'm trying to understand the right way to structure modules in OCaml, and I wonder if you have any feedback... I'm used to SML where we just have signatures and structures, but in OCaml there is another layer: the notion of an interface (.mli) and its implementation (.ml). Interfaces include specifications of signatures.

In SML, for one unit of code I would write a .sig file that has the signature, and a .fun/.sml file that contains the corresponding functors and/or structures.

In OCaml, should I have a .mli file that includes signatures and declarations of structures? And then write the signatures again in the .ml file? (For what it's worth, I'm most interested in how to properly structure developments, and I'm not too worried about the potential duplication.) Just curious about what is idiomatic.

[ghost]

In OCaml, should I have a .mli file that includes signatures and declarations of structures? And then write the signatures again in the .ml file? (For what it's worth, I'm most interested in how to properly structure developments, and I'm not too worried about the potential duplication.) Just curious about what is idiomatic.

@jonsterling Good question. I'm not sure what is really the most idiomatic way to do things as far as the larger community is concerned but I do usually try to provide both .ml and .mli files even though this sometimes means there is a duplication of code.

You can take a look at how I have structured things in yggdrasil for inspiration if it helps. Don't forget about module type of (here for example) since this can save you a lot of work.

For a more elaborate example you could also check out ocaml-cats. This is one where I tried to be pretty methodical about overall structure.

[jonsterling]

@freebroccolo Thank you, that's very helpful!

[jonsterling]

I'm going to merge this now and we can make further improvements to the arrangement of modules at any time.

Just to record something, I want to say that I think it was a good idea to separate the Var constructor from the term signature! This makes it possible to implement all syntactic operations generically, and disentangles the nest of modules that we had in the previous version of the elaborator framework. I guess it also makes sense because there is nothing that guarantees for an arbitrary model of a theory that Var should be implemented as a constructor!

Another thing that helped in this redesign was to replace the Ref of key * subst constructor in the internals with Ref of [`Defer of key * subst | `Done of t] ref. This means that when we do a lookup-and-subst during out, we can just store that result directly in the term, rather than needing some complicated scheme to rewrite an entry in the proof state.

Doing this memoization should be justified, by the way, by the fact that proof state transitions are required to be monotone. In particular, the only thing you're allowed to do to a proof state (besides adding new cells) is replace an Ask with a Ret. So updates don't actually invalidate this cached result (I think). That's crucial.