Three Dollar Quill

Okay, I let things go late tonight, so I'm going to try to just jot down some thoughts.

After the entry last night, I redid things a bit. Now, there's a single module per property (ish), and a given property and (currently) magma can be combined in a functor to produce a module that determines whether a collection of values in the magma represent a contradiction of the property. There are at least two directions that I need (want?) to take this.

• What does it look like when I make the structure more complicated? The obvious place to start here is to single out a value of the magma's type, and to devise a property check that the designated value is an identity element.
• Constructing these predicates is not the end goal. My gut tells me I want the ability to take the attestations for the property of some modules, combine those modules into a compound module, and also combine those attestations into a compound attestation.

I've been trying to mentally line up the different parts that could be involved there. Here's one idea that just popped into my head, and I'll lay it out, pop into the playground, and say whether it seems reasonable:

• Assume that, when there's a compound or derived property at play, the user knows about it, so it's fine to do some one-off stuff.
• A compound module functor knows how the component modules get put together, so it also knows how to put together corresponding attestations. (It also has the knowledge to do more elaborate stuff, like combining structures that carry out different operations on the same underlying set.)
• So, if I'm using modules to represent both algebraic structures and assertions about them, does that mean that my "combine structures" functor can define a "combine assertions" functor?

...

Oh, yes.

*Ahem*

I'm still getting a handle on what OCaml will and won't let me do. When I was first messing around with this space, I was trying to accomplish things in a way that very much did not fit with what OCaml lets you do, and it kind of seems like there isn't a way to make it do that, because the syntax that expressed my ideas already meant something different. So it's really gratifying to see a way forward to accomplishing this stuff.

I can try to do this stuff over the next few days, and see what falls out. For now, I'm going to wrap up.

Good night.