The algebra and calculus of algebraic data types (2015) | Hacker News Reader

The algebra and calculus of algebraic data types (2015)

codewords.recurse.com

128 pointsthunderbong45 comments

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 would be interested in reading more if you manage to find the paper(s).

This reminds me of a section from a category theory text that I encountered.

It had similarly 'crazy' what-ifs, including one where the author used the quadratic formula and interpreted some meaning from it.

It was a course only text, not distributed outside the university as far as I know.

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!

Yeah because aren't the numbers associated with the types related to cardinality?

> Nat has countably many inhabitants. And one more than countably infinite is countably infinite!

Two sets having the same cardinality (number of inhabitants) is insufficient to prove that two sets are equal. There is an additional condition that they all share the same elements.

I read 1 + Nat as: map each element in the Naturals to its successor (i.e. Nat - {0}). 0 is in Nat, but 0 does not exist in "1 + Nat" since it got mapped to 1.

This would be true if the set we were working with were the Integers instead of the Naturals.

This is incorrect.. the equation represents the number of elements in Nat based on its definition.

Integers could be Int = Nat | Neg Nat. So Int = 2 * Nat. Your logic would presumably interpret this as even naturals.. but ya

> Your logic would presumably interpret this as even naturals.. but ya

My logic comes from a Math background. Take any Abstract Algebra class and this notation is common.

For example: https://math.stackexchange.com/questions/1378174/how-to-deno....

To say the least I take numerous issues with the notation used, but I accept it. Since the integers and the naturals have the same cardinality, we have that Int = Nat.

I'm always confused as to why people want to be able to do arithmetic with infinity. Infinity isn't a number.

> countably infinite

Countably infinite means you can count to any particular element of a set in finite time, even though there is no end to the pattern of elements in the set.

You cannot count to infinity plus one in finite time.

That's not the attitude which leads to inventing the negative numbers, for example! The ordinals are useful and it's very reasonable to call them "numbers"; and I'm told that the surreal numbers are useful, although I've never actually used them.

Infinity is not a number but transfinite numbers [1] like omega [2] or aleph-null [3] are. They are just as number as 0, 1, -5, 6/7, pi, i, or quaternion numbers. What is a "number" is not well-defined, any mathematical algebraic object can be called a number with some justification. Mathematicians just don't do it anymore, they just call it "X Algebra" instead of "X Numbers" but there is no fundamental distinction. From this perspective, arithmetic with infinity is not only possible but also extremely useful for Programming Language Theory, e.g. for Dependent Type Theory.

[1] https://en.wikipedia.org/wiki/Transfinite_number

[2] https://en.wikipedia.org/wiki/Ordinal_number#Ordinals_extend...

[3] https://en.wikipedia.org/wiki/Aleph_number#Aleph-null

A set is "countably infinite" if you can construct a one to one mapping from the set to the natural (counting) numbers.

The natural numbers are of course countably infinite, but so are even numbers, prime numbers, fractions, algebraic numbers and lots of other kinds of numbers that people want to do arithmetic with. "Uncountably infinite" sets can't be put into a one to one correspondence with the naturals, no matter how you produce to produce such a mapping, it's always possible to produce a number in the set which wasn't part of it. Real numbers being the prototypical example of that, but the power set (the set of all the subsets) of the naturals is, also.

People do arithmetic with all kinds of things that "aren't numbers". Math isn't restricted to working with numbers.

Just to be pedantic: you mean ‘one-to-one and onto’, otherwise you’re only capturing countability rather than being countably infinite.

Countably infinite doesn’t mean you can count to any particular element in finite time; such a definition would depend on an ordering which cardinality (and, in particular, countability) shouldn’t.

For example, uncountable sets can exhibit the property you mention: you count to x via the (very) finite sequence {x} for any element x of the set of real numbers.

Conversely, countable sets (even if you restrict such enumerations to a certain ordering) don’t in general have this property: ordering the integers by [x < y iff x < y (mod 2) or x < y if x = y (mod 2)] (that is, taking two isomorphic copies of the integers, identified with the even and odd integers respectively, juxtaposed side by side), the sequence {0,2,4,6, …} fails to arrive at 1 no matter how far you count along. So there’s an element we can’t count to in ‘finite time’.

The property you seem to be alluding to, that ‘the set admits a total order such that every element can be reached in finitely many steps starting at the first element’ actually corresponds to the order type of the natural numbers — often called ω. It’s countable, but there are many, many (in fact, uncountably many) more sets with this cardinality that don’t have that property.

The proper definition of ‘countably infinite’ is simply that the set can be placed in bijection with the natural numbers. This has nothing (directly) to do with ordering.

> The proper definition of ‘countably infinite’ is simply that the set can be placed in bijection with the natural numbers. This has nothing (directly) to do with ordering.

Does it not imply that there exists an ordering which reaches each value in finite time? That's how I'd straightforwardly read GP's comment. A given countable set under its 'natural' ordering might not have order type ω, but there will always exist some alternative ordering with type ω.

(And indeed, the existence of such an ordering implies that the set is countable.)

Yes. You're correct. I realised this some time after writing my comment.

So it actually does work as a definition, if you phrase it properly.

I guess it's just equivalent to the observation that ω has the property that every initial segment (i.e. every subset of the form {0, 1, ..., n}) is finite.

So you could say: a set S is countable if it admits an ordering that makes it 'covered by all finite initial segments'.

...but this boils down to saying the set admits an ordering that makes it isomorphic to some n, or ω... which just means it's countable in the usual sense.

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.

A ring forms an Abelian group with just its additive operation, so you basically have subtraction there. As far I can tell the structure we have formed by these datatypes is a semiring.

Ah also the multiplication operation isn't commutative, since struct { int A; float B; } is different from struct { float A; int B; }. So maybe it's a "noncommutative semiring".

Ring don’t require multiplication to commute, only addition. (Square) matrices make just fine rings despite noncommutativity. But the semiring of types does have commutative multiplication (only a semiring, or "rig", because the lack of additive inverses).

Those two structs are equivalent (isomorphic) in the algebraic sense – names don’t matter, and order (indices are just a kind of names) doesn’t either. (a, b) = a x b = b x a = (b, a).

Technically yeah but there is a natural isomorphism between struct { int A; float B; } and struct { float B; int A; } so if you're willing to do everything up to isomorphism (which is usually completely fine and standard) then you get a commutative semiring.

You have to work up to isomorphism anyway even to get a noncomutative semiring because technically the multiplication isn't exactly associative only associative up to an isomorphism.

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?

> Specifically, I question if it is really how most people think in terms of programming.

No, of course not. Algebra is only useful when you want to manipulate that exact thing, and most programmers never do any complex manipulation of types.

Compiler programmers writing powerful type systems do think that way.

> There are algebraic ideas in chemistry, but I would struggle to say how they look the same as this.

Oh no, they don't. The algebra of Quantum Mechanics is way weirder than that. (At least when you move after simple rotations and step-potential wheels.)

Just to make sure I'm not misreading, this is largely an agreement? I think I'm fully in agreement that a compiler class should cover this. I will also hasten to say that I find it a fun topic, such that I don't think it should not be offered elsewhere. I just don't know that I can see a lot of application to general programming.

> I think I'm fully in agreement that a compiler class should cover this.

Then yes, I agree with you.

Here's a very simple example:

A user can have one of two roles: Normal or Admin. You can model this as:

  - User = Name x Password x Role
  - Role = Normal + Admin

or you can multiply it out and get

  - User = Admin or Normal
  - Admin = Name x Password
  - Normal = Name x Password

Which you should choose depends on the application. The second representation forces you to consider at every step if you have an Admin or Normal user, which is better for security. The first representation is more convenient when you don't care about the role.

I do these transformations a lot when modelling things. They are trivial, but if you don't understand the underlying algebra you might not see them (in the same way the developers who aren't used to sum types tend to be blind to them.)

Does that help?

What would be User x Role?

Is it (Name x Password x Role) x (Normal + Admin) = ?

What data-structure would that represent?

If User = Name x Password x Role and Role = Normal + Admin

Then

   (Name x Password x Role) x (Normal + Admin)
  = (Name x Password x Role) x Role
  = Name x Password x Role x Role

(See the normal rules of algebra apply)

In Ocaml you would write

  type Something = User * Role

  type Something = Name * Password * Role * Role

In Typescript you would have something like

  type Something = { user: User, role: Role }

  type Something = { name: Name, password: Password, role1: Role, role2: Role }

These two types are isomorphic (they have the same structure when you ignore irrelevant details) but you'd program with them slightly differently.

Neither type makes a great deal of sense, but it's what you asked for. :-)

I'm not clear that I see the benefit of the techniques here? For one, it is not necessarily obvious that the "or (|)" is not a distributive property. It is, instead, a population description? As such, it seems like it leads to a very weird statements compared to what you would get in other uses.

For example, if instead of Role, it was IsAdmin, and IsAdmin = True | False, then your application here gets you the odd True = Name x Password. What does that even mean?

It also has an odd one of what if Role = Normal + Admin + SuperAdmin, but User is still Admin | Normal? What does that even mean?

Or is + (Writing or was a typo)

User has a Name, Password, and a Role, which gives

  User = Name x Password x Role

Role is Normal or Admin. Formally:

  Role = Normal + Admin

Now substitute

  User = Name x Password x (Normal + Admin)

Multiply out

  User = (Name x Password x Normal) + (Name x Password x Admin)

I added an extra step where I named some of the components.

If you understand how this can be represented in code as an algebraic data type, you will see these two different representations have different properties when you come to program with them.

If you don't, I'm afraid this text box does not contain enough space. Chapter 2 of https://scalawithcats.com/ goes through this in much more detail.

Cool, was curious why you had + and "or". I was assuming both are the same as | in the linked article. (I am further assuming you are largely working on the "left hand side" per the article?)

The rest of your math, I largely followed, but I can't see where `Normal = Name x Password` results. Nor do I see what it would communicate. This is why I dropped instead to Boolean = True | False. If I substitute that in your statements, I get `True = Name x Password`. And I don't see how that means anything. :(

Name and Password are probably going to wrap the String type. Admin and Normal don't have data associated with them. They are just flags (or tags, depending on the terminology you are used to.)

So when we write

  User = (Name x Password x Normal) + (Name x Password x Admin)

we know that Normal and Admin distinguish two otherwise identical cases. So with a bit of substitution we can write

  User = Normal + Admin
  Normal = (Name x Password) 
  Admin = (Name x Password)

True + False is isomorphic to Normal + Admin, but if you aren't used to working in a language with algebraic data types you might not be used to thinking in this way.

In Haskell you'd write something like

  data User = Normal Admin Password | Admin Name Password

You could equally write

  data User = True Admin Password | False Name Password

because True and False are just tags, distinct from their use in the boolean type. This would just really confusing to other programmers.

I had a jest, at one point, where I would assume you are not modeling a password in your system. :D I'm assuming you'd instead model an AuthenticatedUser or some such. To that end, I'm fine with giving leeway to the modeling here. We are going for pedagogy.

To that end, if this is a matter of going fast due to constraints of a message board, I am fine. My specific confusion was at the start where you had `Admin = Name x Password`. I'm not at all clear on what that would communicate to me in the types of any variables I would have in my code.

Have you used a language with algebraic data types? I assumed some familiarity, and also with the terminology sum and product types.

Admin = Name x Password defines a type called Admin that has a Name and a Password.

In OCaml I would write something like

  type Admin = Name * Password

In Scala I'd write

  final case class Admin(name: Name, password: Password)

The construction

  User = Normal + Admin
  Normal = (Name x Password) 
  Admin = (Name x Password)

in words is:

  A User is Normal or Admin
  A Normal (User) is a Name and a Password
  An Admin (User) is a Name and a Password

In Scala

  enum User:
    case Normal(name: Name, password: Password)
    case Admin(name: Name, password: Password)

In OCaml

  type User =
     Normal of Name * Password
   | Admin of Name * Password

This all makes sense, at a basic pass. But what does it tell me to claim that an Admin is a Name and a Password? (It probably doesn't help that I'm used to role based permissions where you will emphatically not have a name associated with the authorization. You should be able to trace it back to an authentication, which will have a name, but those are different.)

I'm also confused with these assertions, as with this formulation, you make it far too easy to think that a User is an Admin. Due to the norm for equality rules being that they are transitive.

Again, if this is just a shortcoming of this particular example, I'm fine with that. I am not trying to tear down the whole idea over the example. I literally just don't understand what it would mean for my model to say that an admin is a name and a password. Transitively, that feels very dangerous when considered in the way I'm used to modeling authentication and authorization.

I'm just trying to make an allusion to how people might model the data in a simple CRUD app. I think you're getting too concerned with the details wrt your prior experience. Make it Pet = Name x Weight x Species, and Species = Dog + Cat if you prefer.

This is largely fair. Apologies I didn't make it clearer that my question here was specific to the example.

I think one of the most critical issues with thinking about ADTs in terms of an algebra is that they lack inverse operations which are otherwise an extremely critical component of how we conceive mathematics. A disjoint union type is formally equivalent to addition, but disunion is never defined, we are given no formal representation of subtraction. The same is given for cognates of division, of logarithms and roots (what those might look like is an interesting, if oft. neglected manner of research)

There's (somewhat) good reasons we don't define these operations, of course. All the same, without being able to represent these inverse operations, the ease of which it maps to familiar notions of the typical algebras we're used to ends up thrown out the window.

The algebra metaphor makes a bit more sense when you move beyond ADTs into more advanced levels of type-theory. Dependent types are a fair bit beyond a mere algebra, instead being more like a complete metalanguage akin to higher-order logic.

I think this is underscoring my concern with this as a pedagogical thing. I have seen people try very hard to find analogs with basic algebra. And... by people, I mainly mean younger me. Building algebras is, I think, still a very valuable thing if you can do it. Often times, though, the goal is not to fully mimic the basic algebra of grade school, but to map out what is doable with the abstractions that you have.

The algebra of types is a semiring, which is a generalization of a ring that drops the requirement of an additive inverse, just as a ring is a generalization of a field that doesn’t require a multiplicative inverse. Semirings are pretty common in math – hell, natural numbers form (only) a semiring, having neither type of inverse! Can’t get more fundamental than that. And of course the connection between naturals (counting numbers) and types is evident from the fact that we started this whole exercise by counting inhabitants and defining equivalent based on that!

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

Reply on news.ycombinator.com