## Lens as a Divisibility Relation: Goofin’ Off With the Algebra of Types

Types have an algebra very analogous to the algebra of ordinary numbers (video). This is the basic table of correspondences. Code with all the extensions available here.

One way to see that this makes sense is by counting the cardinality of types built out of these combinators. Unit is the type with 1 inhabitant. Void has 0 inhabitants. If `a` has $n$ and `b` has $m$ possible values, then `Either a b` has $n + m$ inhabitants, `(a,b)` has $n*m$ and there are $n^m$ possible tabulations of a->b. We’re gonna stick to just polynomials for the rest of this, ignoring a->b.

Another way of looking at this is if two finitely inhabited types have the same number of inhabitants, then the types can be put into an isomorphism with each other. In other words, types modulo isomorphisms can be thought as representing the natural numbers. Because of this, we can build a curious proof system for the natural numbers using ordinary type manipulation.

In addition, we also get a natural way of expressing and manipulating polynomials.Polymorphic types can be seen as being very similar to polynomial expressions with natural coefficients `N[x]`. The polymorphic type variables have the ability to be instantiated to any value, corresponding to evaluating the polynomial for some number.

The Lens ecosystem gives some interesting combinators for manipulating this algebra. The type `Iso' a b` contains isomorphisms. Since we’re only considering types up to isomorphism, this `Iso'` represents equality. We can give identity isomorphisms, compose isomorphisms and reverse isomorphisms.

We can already form a very simple proof.

Now we’ll add some more combinators, basically the axioms that the types mod isos are a commutative semiring. Semirings have an addition and multiplication operator that distribute over each other. It is interesting to note that I believe all of these `Iso'` actually are guaranteed to be isomorphisms ( `to . from = id` and `from . to = id` ) because of parametricity. `from` and `to` are unique ignoring any issues with bottoms because the polymorphic type signature is so constraining. This is not usually guaranteed to be true in Haskell just from saying it is an `Iso'`. If I give you an `Iso' Bool Bool` it might actually be the `iso (const True) (const True)` for example, which is not an isomorphism.

There are also combinators for lifting isomorphisms into bifunctors: `firsting`, `seconding`, and `bimapping`. These are important for indexing into subexpressions of our types in a point-free style.

Here is a slightly more complicated proof now available to us.

We can attempt a more interesting and difficult proof. I developed this iteratively using `. _` hole expressions so that GHC would tell me what I had manipulated my type to at that point in my proof.

The proof here is actually pretty trivial and can be completely automated away. We’ll get to that later.

If `Iso'` is equality, what about the other members of the Lens family? Justin Le says that `Lens s a` are witness to the isomorphism of a type `s` to the tuple of something and `a`. `Prism` witness a similar thing for sums. Once we are only considering types mod isos, if you think about it, these are expressions of two familiar relations on the natural numbers: the inequality relation and the divisibility relation

Mathematically, these relations can be composed with equalities, just like in the lens hierarchy `Lens` and `Prism` can be composed with `Iso`. Both form a category, since they both have `id` and `(.)`.

Here are a couple identities that we can’t derive from these basic combinators. There are probably others. Woah-ho, my bad. These are totally derivable using id_mul, id_plus, mul_zero, _1, _2, _Left, _Right.

Pretty neat! Random thoughts and questions before we get into the slog of automation:

• Traversal is the “is polynomial in” relation, which seems a rather weak statement on it’s own.
• Implementing automatic polynomial division is totally possible and interesting
• What is the deal with infinite types like `[a]`? `Fix`. I suppose this is a theory of formal power series / combinatorial species. Fun combinatorics, generatingfunctionology. Brent Yorgey did his dissertation on this stuff. Wow. I’ve never really read this. It is way more relevant than I realized.
• Multivariate polynomial algorithms would also be interesting to explore (Grobner basis, multivariate division)
• Derivatives of types and zippers – Conor McBride
• Negative Numbers and Fractions?
• Lifting to rank-1 types. Define Negative and Fractions via Galois connection?

Edit: /u/carette (wonder who that is ðŸ˜‰ ) writes:

“You should dig into
J Carette, A Sabry Computing with semirings and weak rig groupoids, in Proceedings of ESOP 2016, p. 123-148. Agda code in https://github.com/JacquesCarette/pi-dual/tree/master/Univalence. A lot of the algebra you develop is there too.

If you hunt around in my repos, you’ll also find things about lenses, exploring some of the same things you mention here.”

Similar ideas taken further and with more sophistication. Very interesting. Check it out.

## Automation

Our factor example above was quite painful, yet the theorem was exceedingly obvious by expansion of the left and right sides. Can we automate that? Yes we can!

Here’s the battle plan:

• Distribute out all expressions like $a*(b+c)$ so that all multiplication nodes appear at the bottom of the tree.
• Reduce the expression by absorbing all stupid $a*1$, $a*0$, $a+0$ terms.
• Reassociate everything to the right, giving a list like format
• Sort the multiplicative terms by power of the variable

Once we have these operations, we’ll combine them into a `canonical` operation. From there, most equality proofs can be performed using the `rewrite` operation, which merely puts both sides into canonical form

Once we have those, the painful theorem above and harder ones becomes trivial.

Now we’ll build the Typeclasses necessary to achieve each of these aims in order. The Typeclass system is perfect for what we want to do, as it builds terms by inspecting types. It isn’t perfect in the sense that typeclass pattern matching needs to be tricked into doing what we need. I have traded in cleverness and elegance with verbosity.

In order to make our lives easier, we’ll need to tag every variable name with a newtype wrapper. Otherwise we won’t know when we’ve hit a leaf node that is a variable. I’ve used this trick before here in an early version of my faking Compiling to Categories series. These wrappers are easily automatically stripped.

A common pattern I exploit is to use a type family to drive complicated recursion. Closed type families allow more overlap and default patterns which is very useful for programming. However, type families do not carry values, so we need to flip flop between the typeclass and type family system to achieve our ends.

Here is the implementation of the distributor `Dist`. We make `RDist` and `LDist` typeclasses that make a sweep of the entire tree, using `ldist` and `rdist` as makes sense. It was convenient to separate these into two classes for my mental sanity. I am not convinced even now that I have every case. Then the master control class `Dist` runs these classes until any node that has a `(*)` in it has no nodes with `(+)` underneath, as checked by the `HasPlus` type family.

Next is the `Absorb` type class. It is arranged somewhat similarly to the above. Greedily absorb, and keep doing it until no absorptions are left. I think that works.

The Associators are a little simpler. You basically just look for the wrong association pattern and call `plus_assoc` or `mul_assoc` until they don’t occur anymore, then recurse. We can be assured we’re always making progress if we either switch some association structure or recurse into subparts.

Finally, the `SortTerm` routine. `SortTerm` is a bubble sort. The typeclass `Bubble` does a single sweep of swapping down the type level list-like structure we’ve built. The `SortTerm` uses the `Sorted` type family to check if it is finished. If it isn’t, it call `Bubble` again.

Hope you thought this was neat!