4 ms·

I've always thought a nifty thing about algebraic data types is the ability to deduce their size (in the set theoretic sense, the number of possible elements) b

by kccqzy 2y ago

I've always thought a nifty thing about algebraic data types is the ability to deduce their size (in the set theoretic sense, the number of possible elements) by algebra. Consider Bool which is a fundamental primitive type with size 2. Now consider the product type Bool × Bool × Bool (a three-tuple), it's clear that it has size 2×2×2=8. On the other hand if we have the sum type Bool + Bool + Bool (a discriminated union), it's also clear it has size 2+2+2=6. And this works with recursion too. The list type whose element type is A is defined as either Nil or an element plus the remainder of the list: that's exactly L(A)=1+A*L(A). And that directly solves to L(A)=1/(1-A). If you've studied generating functions or even just Taylor series, you know this can be expanded into 1+A+A^2+A^3+… which perfectly matches the intuition of a list having any number of elements. What if I want to define a special list that only allows even number of elements? It would be L(A)=1+A*A*L(A), or 1/(1-A^2) which expands to 1+A^2+A^4+… Both of course are "infinite" but it allows us to distinguish precisely what kind of "infinity."

kqr 2y ago
This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cases) with three cases, we see immediately there's a singularity in there which represents at least two of the possible values of the original, i.e. we won't be able to losslessly round trip.
- perihelions 2y ago
  This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by observing that the cardinalities are equal as algebraic expressions, ( |A|^|A| )^|A| = |A|^( |A|*|A| ). That one's just "currying" [0]. [0] https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/Currying
  - Sharlin 2y ago
    Yep, that’s one of the more mind-blowing "tricks" as it were. Maybe less moreso, but still nifty, is that |T -> bool| = |bool|^|T| = 2^|T| …which also happens to be the number of subsets of a set of size |T|. And indeed that’s what a predicate function is, a subset-generator; for every subset there is exactly one predicate that picks the members of that subset from the larger set.
    - gpderetta 2y ago
      That's true for any type, not just bool right? And is equivalent of to the observation that any pure function can be replaced by a lookup table.
      - Sharlin 2y ago
        Sure, any function T -> U partitions T into |U| subsets. But the case where |U|=2 is special because 2^N is special in being the number of subsets of a set of size N.
- weitendorf 2y ago
  The thing about isomorphisms between algebraic structures is that they require a representational+inversible mapping (what you mentioned) that preserves relations (something you didn't mention). That distinction is actually relatively important in programming because you might be using something like polymorphism to operate on two representationally equivalent types in different ways. If you have a base class CollidableObject that both PoolBall and GlobOfHoney extend, they could be representationally equivalent (both having two vector member fields, one for Position and one for Velocity) but with different implementations of CollidableObject::HandleCollision(CollidableObject& target) to reflect the fact that PoolBall can elastically collide with certain kinds of targets but GlobOfHoney only collides inelastically. So you'd not want to treat them as isomorphic. I'm mostly just being pedantic but one of my pet peeves is when programmers use terms like Isomorphism or Vector in a way that is partly but not entirely true to the mathematical definition. I think "bijection" is a better term for what you're talking about, because it's both necessary and sufficient for information-preserving mapping between types.
syrak 2y ago
Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually the original meaning of it afaik, and then I went to look for a source for it and that grew into this whole blogpost.
- steego 2y ago
  First of all, thank you for writing that up!!! Disclaimer 1: I have the same last name as Burstall's collaborator, Joseph Goguen. If we're related, it's VERY distant, so I truly can't add anything. Disclaimer 2: I'm going to tie this back into algebras. Setup 1: However, I have been a little obsessed with Burstall and Goguen lately and I've been SLOWLY working through some papers and trying to make sense of it. I'm just an F# programmer who likes languages, not an academic. Setup 2: I've known about Burstall/Goguen for some time, but I never understood the gravity of their respective work until recently. And I have quite literally been annoying with my tech friends and family with all my "Oh my god!" moments as I've been going papers and festschrifts. This whole time, I haven't been sure if I've been interpreting what I'm reading correctly, so your post has been wonderful in settling some of that. I understand that some people may resist the idea of describing algebraic data types as analogous to the fundamental theorem of arithmetic for types. Burstall and Goguen were motivated by creating tools and systems built on solid foundations, such as universal algebras, to utilize analytical tools like logic systems and category theory for deeper insights. However, I believe they were particularly focused on how algebraic data types model the cardinality of state spaces and transitions between states for this reason: They were designing a specification system that helped working programmers design systems accomplish two things (In today's parlance): 1. Make invalid states impossible. 2. Make invalid transitions between states impossible. While learning Maude (OBJ's successor), I've been particularly fascinated with how its parent language let you define very fine grained domains. And it makes sense, because if you're going to search through that domain to find counter-examples violating your theories, it makes sense to reduce the search space proactively. But what really drove that for me (and maybe I'm projecting here), is how that seemed to correspond to a little program I wrote that constructed a bijection between the natural numbers and all closed lambda functions. https://gist.github.com/sgoguen/46200419194eb29b82079b0804e58c34?permalink_comment_id=4834713#gistcomment-4834713 https://gist.github.com/sgoguen/46200419194eb29b82079b0804e5... But what really convinces me that they had that in mind is how Maude and OBJ let you add attributes to constructors to identify them as associative or commutative or whether it has an "id" where the impact of these attributes on the constructors actually reduces the state space. Again, I could be projecting here, but I would love to hear your thoughts and I am excited to read your next post! Thank you!
justinpombrio 2y ago
And you can use this algebra to refactor data types! It's a surprisingly deep topic. I wrote a blog post about it: https://justinpombrio.net/2021/03/11/algebra-and-data-types.html https://justinpombrio.net/2021/03/11/algebra-and-data-types.... And someone else wrote a related blog post: https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types https://codewords.recurse.com/issues/three/algebra-and-calcu...
marcosdumay 2y ago
I really don't like this view (but looks like I'm a small minority). Types shouldn't have an algebra similar to numbers, they should have an algebra similar to sets. While for numbers A + A + A = 3A, on sets A ∪ A ∪ A = A. Types are all about predicate satisfaction, and predicates don't change their value because they can be proven in more than one way. In practice, defining type sums as tagged sums leads to your algebra, and also leads to a lot of confusion between structure and denomination that would be completely avoided if sums and tags were independent operations.
- paholg 2y ago
  The difference is mostly a matter of perspective, isn't it? In Rust, if I have ``` enum Foo { A(u32), B(u32), C(u32), } ``` Then the number of representable states is deduced my an "algebra of numbers", but the size is deduced by an "algebra of sets". For example, the size of Foo is just 8 (4 bytes for u32, and 4 for the tag + alignment).
  - marcosdumay 2y ago
    Given the types: I = A + B; J = C; X = A; Y = B + C Is I + J the same type as X + Y? If your types are tagged, they aren't. Because that's what tags do.
    - paholg 2y ago
      Okay? I don't know what point you're making.
    - bombela 2y ago
      My answer would be: No they are not the same type. Yes they have the same amount of bits representing them. They might have different RAM usage because of alignment.
    - xigoi 2y ago
      > Is I + J the same type as X + Y? They are not the same, but they are isomorphic. Just like with (A×B)×C versus A×(B×C).

by kccqzy 2y ago

kqr 2y ago

This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cases) with three cases, we see immediately there's a singularity in there which represents at least two of the possible values of the original, i.e. we won't be able to losslessly round trip.

perihelions 2y ago
This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by observing that the cardinalities are equal as algebraic expressions, ( |A|^|A| )^|A| = |A|^( |A|*|A| ). That one's just "currying" [0]. [0] https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/Currying
- Sharlin 2y ago
  Yep, that’s one of the more mind-blowing "tricks" as it were. Maybe less moreso, but still nifty, is that |T -> bool| = |bool|^|T| = 2^|T| …which also happens to be the number of subsets of a set of size |T|. And indeed that’s what a predicate function is, a subset-generator; for every subset there is exactly one predicate that picks the members of that subset from the larger set.
  - gpderetta 2y ago
    That's true for any type, not just bool right? And is equivalent of to the observation that any pure function can be replaced by a lookup table.
    - Sharlin 2y ago
      Sure, any function T -> U partitions T into |U| subsets. But the case where |U|=2 is special because 2^N is special in being the number of subsets of a set of size N.
weitendorf 2y ago
The thing about isomorphisms between algebraic structures is that they require a representational+inversible mapping (what you mentioned) that preserves relations (something you didn't mention). That distinction is actually relatively important in programming because you might be using something like polymorphism to operate on two representationally equivalent types in different ways. If you have a base class CollidableObject that both PoolBall and GlobOfHoney extend, they could be representationally equivalent (both having two vector member fields, one for Position and one for Velocity) but with different implementations of CollidableObject::HandleCollision(CollidableObject& target) to reflect the fact that PoolBall can elastically collide with certain kinds of targets but GlobOfHoney only collides inelastically. So you'd not want to treat them as isomorphic. I'm mostly just being pedantic but one of my pet peeves is when programmers use terms like Isomorphism or Vector in a way that is partly but not entirely true to the mathematical definition. I think "bijection" is a better term for what you're talking about, because it's both necessary and sufficient for information-preserving mapping between types.

syrak 2y ago

Author here. It's funny you mention this. I was (am still) writing a post about it, and I went on a rant that while it's a (fun!) way to do "algebra with types", it's not actually the original meaning of it afaik, and then I went to look for a source for it and that grew into this whole blogpost.

steego 2y ago
First of all, thank you for writing that up!!! Disclaimer 1: I have the same last name as Burstall's collaborator, Joseph Goguen. If we're related, it's VERY distant, so I truly can't add anything. Disclaimer 2: I'm going to tie this back into algebras. Setup 1: However, I have been a little obsessed with Burstall and Goguen lately and I've been SLOWLY working through some papers and trying to make sense of it. I'm just an F# programmer who likes languages, not an academic. Setup 2: I've known about Burstall/Goguen for some time, but I never understood the gravity of their respective work until recently. And I have quite literally been annoying with my tech friends and family with all my "Oh my god!" moments as I've been going papers and festschrifts. This whole time, I haven't been sure if I've been interpreting what I'm reading correctly, so your post has been wonderful in settling some of that. I understand that some people may resist the idea of describing algebraic data types as analogous to the fundamental theorem of arithmetic for types. Burstall and Goguen were motivated by creating tools and systems built on solid foundations, such as universal algebras, to utilize analytical tools like logic systems and category theory for deeper insights. However, I believe they were particularly focused on how algebraic data types model the cardinality of state spaces and transitions between states for this reason: They were designing a specification system that helped working programmers design systems accomplish two things (In today's parlance): 1. Make invalid states impossible. 2. Make invalid transitions between states impossible. While learning Maude (OBJ's successor), I've been particularly fascinated with how its parent language let you define very fine grained domains. And it makes sense, because if you're going to search through that domain to find counter-examples violating your theories, it makes sense to reduce the search space proactively. But what really drove that for me (and maybe I'm projecting here), is how that seemed to correspond to a little program I wrote that constructed a bijection between the natural numbers and all closed lambda functions. https://gist.github.com/sgoguen/46200419194eb29b82079b0804e58c34?permalink_comment_id=4834713#gistcomment-4834713 https://gist.github.com/sgoguen/46200419194eb29b82079b0804e5... But what really convinces me that they had that in mind is how Maude and OBJ let you add attributes to constructors to identify them as associative or commutative or whether it has an "id" where the impact of these attributes on the constructors actually reduces the state space. Again, I could be projecting here, but I would love to hear your thoughts and I am excited to read your next post! Thank you!

justinpombrio 2y ago

And you can use this algebra to refactor data types! It's a surprisingly deep topic. I wrote a blog post about it: https://justinpombrio.net/2021/03/11/algebra-and-data-types.html https://justinpombrio.net/2021/03/11/algebra-and-data-types.... And someone else wrote a related blog post: https://codewords.recurse.com/issues/three/algebra-and-calculus-of-algebraic-data-types https://codewords.recurse.com/issues/three/algebra-and-calcu...

marcosdumay 2y ago

I really don't like this view (but looks like I'm a small minority). Types shouldn't have an algebra similar to numbers, they should have an algebra similar to sets. While for numbers A + A + A = 3A, on sets A ∪ A ∪ A = A. Types are all about predicate satisfaction, and predicates don't change their value because they can be proven in more than one way. In practice, defining type sums as tagged sums leads to your algebra, and also leads to a lot of confusion between structure and denomination that would be completely avoided if sums and tags were independent operations.

paholg 2y ago
The difference is mostly a matter of perspective, isn't it? In Rust, if I have ``` enum Foo { A(u32), B(u32), C(u32), } ``` Then the number of representable states is deduced my an "algebra of numbers", but the size is deduced by an "algebra of sets". For example, the size of Foo is just 8 (4 bytes for u32, and 4 for the tag + alignment).
- marcosdumay 2y ago
  Given the types: I = A + B; J = C; X = A; Y = B + C Is I + J the same type as X + Y? If your types are tagged, they aren't. Because that's what tags do.
  - paholg 2y ago
    Okay? I don't know what point you're making.
  - bombela 2y ago
    My answer would be: No they are not the same type. Yes they have the same amount of bits representing them. They might have different RAM usage because of alignment.
  - xigoi 2y ago
    > Is I + J the same type as X + Y? They are not the same, but they are isomorphic. Just like with (A×B)×C versus A×(B×C).