Three Dollar Quill

Okay, I'm kind of out of it right now, but I'd like to work through my ideas for other stuff to try with OCaml. One concept that ML-style modules seem well-suited to representing is that of an algebraic structure, which is something that Missable Mysteries would have/will end up covering.

I've tied myself in knots trying to fit an algebraic structure (admittedly a somewhat complicated one) into typed Python. I think doing it in Rust would require a bunch of newtypes in the general case, because Rust traits are all about "the implementation" of a concept, and some of the really interesting stuff happens when you're explicitly manipulating multiple groups derived from the same set.

Whereas in OCaml, a specific algebraic structure would be a module, a kind of algebraic structure would be a module signature, and a mapping between algebraic structures, such as "forgetting" parts of a structure, would be a functor.

This is slightly short of what I want, because I'm not sure if there's a good statically-analyzable way to handle the axioms of an algebraic structure. So, what I want to see if I can do is to express axioms in a form that a property-based testing library can handle. I searched around a bit, and found qcheck.

I think there are two basic concepts that need to be defined together to write the kind of tests I have in mind:

• An axiom corresponds to a test function.
• An algebraic structure will have some associated types, which need to have some kind of generator to produce values.

I guess all of this is going to take a bunch more modules and functors. Like, given an algebraic structure with some signature, that needs to combine with a generator, which... stuff happens, and eventually a module pops out with a list of tests.

Properties to test include:

• totality
• commutativity
• associativity
• divisibility
• invertibility
• identity
• distributivity
• forgetting properties in different orders results in structures with the same behavior

I'm pretty tired, so I'm going to wrap this up now, and then sketch out exactly how I think this stuff should fit together.

Good night.