The algebra (and calculus) of algebraic data types

Yes, this is a very cool story.

But, fascinatingly, integration does in fact have a meaning. First, recall from the OP that d/dX List(X) = List(X) * List(X). You punched a hole in a list and you got two lists: the list to the left of the hole and the list to the right of the hole.

Ok, so now define CrazyList(X) to be the anti-derivative of one list: d/dX CrazyList(X) = List(X). Then notice that punching a hole in a cyclic list does not cause it to fall apart into two lists, since the list to the left and to the right are the same list. CrazyList = CyclicList! Aka a ring buffer.

There's a paper on this, apologies I can't find it right now. Maybe Alternkirch or a student of his.

The true extent of this goes far beyond anything I imagined, this is really only the tip of a vast iceberg.

I always love this topic.

> Nat = 1 + Nat. This equation is clearly inconsistent, since x=1+x is false for all possible values of x.

Ah, but no, my friend. That equation is false merely for all possible finite values of x. But why impose such a constraint? We've already been identifying a correspondence between certain types and the number of inhabitants they have. Nat has countably many inhabitants. And one more than countably infinite is countably infinite!

Related:

The algebra and calculus of algebraic data types - https://news.ycombinator.com/item?id=17942112 - Sept 2018 (48 comments)

The Algebra of Algebraic data types - https://news.ycombinator.com/item?id=9775467 - June 2015 (40 comments)

> Can we extend the analogy to integration?

Dumb idea: Unzipping?

Differentiation takes as input the overall structure and extracts the behavior at a certain location. Integration takes the behavior at many different locations and returns a coherent picture of the overall structure.

I'm struggling to picture the math. Does this work the way I envision?

For people without some mathematical/language-relevant background, the following preliminaries would be useful;

1) A brief introduction to the Algebra of Types (nice intuitive explanation) - https://code.egym.de/a-brief-introduction-to-the-algebra-of-...

2) Algebraic data type - https://en.wikipedia.org/wiki/Algebraic_data_type

3) Comparison of programming languages (algebraic data type) - https://en.wikipedia.org/wiki/Comparison_of_programming_lang...

That is such a great website! Amazing content throughout.

> Let’s pause for a moment to remember that we’re dealing with types. And the expression 1 / (1 - a) contains both a negative and a fractional type, neither of which have a meaning yet.

This makes me wonder, is there a ring of types? There's addition and multiplication. Division and subtraction aren't necessary to define a ring, so their absence isn't particularly surprising.

I am always torn when I see these discussions. Yes, I fully appreciate a lot of the easy algebra applies to some things. I further appreciate many of the optimizations that can be created by taking advantage of many of these.

However, I have grown skeptical on its pedagogical use in programming. Specifically, I question if it is really how most people think in terms of programming.

I further question if this is how most modelling considers things. An easy example would be chemistry. There are algebraic ideas in chemistry, but I would struggle to say how they look the same as this.

Am I looking past an obvious aide to modelling that these approaches can give? I appreciate how this post acknowledges that there are not obvious uses of integration and such, but I feel that sort of proves my point. There are familiar mathematical tools that are good to use when we can. This does not mean you need to force them onto everything you have.

It would probably help me a ton, if I ever saw these applied to state machines?

This appears to have been published in 2015. Perhaps update the title with the year?