Lawvere theories

L0neGamer:

With the above, it is described as a functor; could we make it into a proper haskell function by just swapping n and a?

Notice that F a has kind Arity -> Type so it definitely can not be a Functor in the strict Haskell Prelude sense. When swapping the arguments, it is nothing but a vector functor of statically known dimension, e.g.

newtype V2 a = V2 (F a Two)

For the functoriality of F a, I did write that objects of Arity are to be thought of as natural numbers, but did not say what the morphisms are. The n-Category Cafe describes it as “the opposite of a skeleton of the category of finite sets”. Hence my use of Pair for what at first glance appears to be a coproduct. (2 is not equal to 1 * 1 but to 1 + 1)

L0neGamer:

Or is this construction not powerful enough for that kind of “proof”, and it’s merely just setting up for quickchecking

I did not intend this to be accessible to proof-checking, just wanted to convey the original idea of Lawvere theory as direct as possible. In any case, what would a “proof” of the laws be? It would, for any particular model of the theory, require knowledge of the particular implementation of model, which would have to be encoded somehow in a form so that a proof checker can analyze it.

There is another technique for algebraic categories, called “generators and relations”. It says that every object of the category is a quotient of a free object over some generators, by relations that honour the algebraic structure, so-called congruence relations. I can imagine that is is easy to prove that a free construction is lawful, thereby shifting the proof burden towards proving that the relations form a congruence. Sadly, relations are hard to work with in computing, due to the existential quantification in the relational composition.