Three Dollar Quill

I'm tired, but here's what I've worked out from reading Wikipedia and messing around:

• There are five-ish basic structures I want to mess with to start with.
• Each of these structures needs a few of its own versions of things:
  • A "witness" module type that constructs a contradiction-checking function from components of the structure.
  • A "witness of" functor that combines an instance of the structure type and the witness type.
  • Functors that construct structure instances out of other structure instances; these functors should themselves provide functors that map from attestations of the components to new attestations for the composite.

The attestation concept has a lot going on, and I'm trying to figure out whether it needs specialized components as well, or if it can be general like some of the support code. An attestation, in my informal thoughts on this, has:

• A structure (module, necessary for typing)
• A property (module, necessary for typing)
• A witness function (probably in a module; derived from structure and property, but I think not in a generalizable fashion)
• The witness module provides an unreduced specimen type; there must also be a partially reduced specimen type
• Fully reduced specimen type
• Mapping from unreduced specimen type to list of partially reduced specimen type
• Function to test reduced specimen types for a contradiction
• Mapping from partially reduced specimen type to fully reduced specimen types

Probably more, there's so much in there... And some stuff that maybe can be moved out of the module interface. I think a bunch of this needs to be structure-specific, so I'll have to figure out how much of it can be factored out.

Okay, that's... a lot. I'm going to wind down and try to take it easy for a while.

Good night.