Three Dollar Quill

Well, I messed around in Peglin, but I'd rather work with OCaml stuff for this post. Let's see about some of the stuff I was thinking about last time.

I decided to start off by trying to make some of the currently not-too-important code I wrote "actually work", and I ran into trouble. Here's the deal. Any algebraic structure that includes a magma can potentially have that magma be commutative. This isn't too important to the main... does anyone call it the Group Theory Cube, or something like that? But it's definitely something that comes up. For example, the trivial group and the cyclic groups are commutative. So, if I'm all like, "I want to mark the loops coming out of this functor as commutative", or whatever, then I need to be able to construct a signature for "a loop, but commutative".

I'm not sure if the way I'm currently trying to express this even makes sense in OCaml. Like, the stuff I'm reading kind of makes it look like "stick stuff onto a random signature" isn't an intended thing, in part because the syntax I'm trying to use is very similar to the syntax for a completely different concept. So, maybe I need some other way to mark "properties that only become apparent by calling the magma operation multiple times". The first thing that I thought of is "something with phantom types", but that doesn't seem to have solved what I think is the actual hard part, of "some magmas can be associative, some can be associative, some can be both, some can be neither". And worse, "what if somebody else thinks of a property to check?"

Maybe if I can figure out how to express "this set contains such and such member" as a type-level assertion, I can turn this idea into "there's a set of properties".

... Or maybe I can swing something with object types. Like, structural typing gets me "I can sort of have type lattice stuff", but I think it's going to discard that information pretty aggressively. I guess the big thing I need to think about is "how do I think this information is even going to get consumed?" Like, I can figure out how to write tests for these properties, but I'm not sure how to express "these properties are needed for this context".

I'll have to think about it, and then commit to something for now.

Good night.