5 ms·

The Algebra of Algebraic Data Types

116 points by crntaylor 14y ago

elliotlai 14y ago
mind blowing, this is just beautiful :)
flebron 14y ago
If you want to see how crazy this can get, know that you can actually take the derivative of a type (with respect to another type), and this yields useful information. See McBride's paper http://strictlypositive.org/diff.pdf http://strictlypositive.org/diff.pdf , or this guy who is discovering it by himself: http://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work http://stackoverflow.com/questions/9190352/abusing-the-algeb...
- cwzwarich 14y ago
  This interpretation of the derivative of a formal power series was known in combinatorics long before people were studying algebraic data types in programming, so I am surprised that McBride presents it as novel.
- crntaylor 14y ago
  "This guy who is discovering it by himself" is me (the OP) about a year ago! Derivatives of types to come in part II or III (or just watch the talk on YouTube: http://www.youtube.com/watch?v=YScIPA8RbVE http://www.youtube.com/watch?v=YScIPA8RbVE)
- kd0amg 14y ago
  Also reminds me of http://www.cs.indiana.edu/~sabry/papers/rational.pdf http://www.cs.indiana.edu/~sabry/papers/rational.pdf
batterseapower 14y ago
Pedants would add that the analogy with number of inhabitants is all a little screwed up in Haskell since bottom is an implicit inhabitant of all data types, which means that e.g. Either Void () has a different number of inhabitants than () and so they cannot strictly speaking be made isomorphic. Strict languages can sidestep this problem to an extent but still end up with "wrong" numbers of inhabitants for e.g. T -> (), since (\_ -> ()) is different from (\_ -> undefined). So the only guys living in pure algebraic bliss are the total functional programmers like the Agda aficionados.
- crntaylor 14y ago
  Yup. I deliberately ignored ⊥ to simplify the presentation (and I make no apologies for doing so!) There are a couple of posts by Dan Piponi where he explores how to count inhabitants of types when you properly account for ⊥: http://blog.sigfpe.com/2008/02/how-many-functions-are-there-from-to.html He does it by counting the number of functions () -> () (where () is of course inhabited by both () and ⊥), and concludes that the number of functions () -> () depends on the semantics of the language: 1 in a total language (like Agda) or in mathematics. 3 in a lazy language (like Haskell) when working completely lazily. 4 in Haskell, when using seq to enforce strictness. 3 in a strict language (like ML). He then goes on to analyse the relationship between point-set topology and computability, showing that the set of computable functions is in a 1-1 correspondence to the set of continuous functions, under the appropriate topology: http://blog.sigfpe.com/2008/01/what-does-topology-have-to-do-with.html http://blog.sigfpe.com/2008/02/what-is-topology.html http://blog.sigfpe.com/2008/03/what-does-topology-have-to-do-with.html Fascinating stuff - but you can see why I decided not to talk about it! Edit: Aha, I just realized who you are, and that we've met before..!
- jonsterling 14y ago
  True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type. So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing. For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.
- dons 14y ago
  http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publicat... Fast and loose reasoning is morally correct.
spacemanaki 14y ago
Ok, pardon my ignorance, but I'm curious if anyone can comment on how this does or doesn't relate to the Curry-Howard correspondence ? The very limited amount of introductory type theory that I've read (mostly Benjamin Pierce's TAPL and Software Foundations) seems to treat Curry-Howard as a deep and fundamental cornerstone, but the only places I've seen the algebraic properties of types explored is in blog posts (http://blog.lab49.com/archives/3011 http://blog.lab49.com/archives/3011). Is there some connection I just haven't figured out yet due to mathematical immaturity? I'm struggling to see the relationship between types as sums, products and exponents, and types as conjunction, disjunction and implication.
- jonsterling 14y ago
  One way to understand it is to think of the “type” side of things (sums, products, exponents) as the sort of things that one needs in order to prove the “propositional” side of things (disjunction, conjunction, implication). So, a term of a sum type will serve as a proof for the corresponding disjunction proposition, and so forth. As to how the number of terms in a given type follows in CH, it's just the number of possible proofs for the corresponding proposition.
- tel 14y ago
  The answer you're looking for is in category theory. For a long time people ad hoc recognized that "products" and "sums" exist in many different domains, but there wasn't a universal method to construct them. Category theory does just that by treating all of these things as special kinds of categories and reading off universal properties which link rings, algebraic data types, logic, sets, topological spaces, etc. etc.
pilgrim689 14y ago
I'm a beginner Haskeller and I'm really enjoying this blog so far. After reading through a few tutorials, it's refreshing to get some theoretical background to it all. It helps make the language more intuitive, even if it's not teaching concrete uses of the theory. Subscribed!
- MBlume 14y ago
  Thank you for causing me to notice that the last two haskell posts I really enjoyed were on the same blog. Also subscribed!
guygurari 14y ago
So the algebra of data types, as described, is simply the algebra of natural numbers. I guess this can't be the whole story because it does not describe types which can get an infinite number of values. But still I wonder, what is the practical advantage of using this simple mathematical structure? What does it buy us? Not trying to be snarky, I just don't see the point.
- crntaylor 14y ago
  Indeed, it's not the whole story. Infinite types and recursive types will come along in part 2! As to the practical advantage - does there have to be one? Isn't the fact that it's intellectually gratifying enough? If you insist, though - I sometimes see the kind of laws I presented used in actual Haskell code. For example, in the Data.Lens package[0] you can consider a lens on a a structure of type a to be composed of a getter and a setter of values of type b data Lens a b = Lens (a -> b, a -> b -> a) which is refactored, using the law (a -> b, a -> c) == a -> (b,c), to look like data Lens a b = Lens (a -> (b, b -> a)) which allows for a more efficient 'modify' operation. It also allows you to notice that lenses are related to the 'Store' comonad[1]: data Store b a = Store (b, b -> a) data Lens a b = Lens (a -> Store b a) on which a lot of the Data.Lens internals are based. [0] https://github.com/ekmett/lens https://github.com/ekmett/lens [1] http://stackoverflow.com/questions/8766246/what-is-the-store-comonad http://stackoverflow.com/questions/8766246/what-is-the-store...
  - guygurari 14y ago
    Thanks for explaining and for the examples. I would like to clarify that by 'practical advantage' I do not mean 'how does this help us write a web app' (although that would be nice), I mean 'how does this help us better understand programming'. In my experience, if you find that a problem admits a mathematical structure, but the structure is very simple, then often the structure does not lead to interesting insights -- it is just a form of taxonomy. This happens for example in my field (theoretical physics), where some objects can be described in fancy ways using category theory. These descriptions do not lead to any practical results, like discovering new mathematical properties of the objects involved. Personally I do not find these descriptions gratifying because, again, they are just taxonomy. There usually needs to be some minimal amount of mathematical structure (like group structure, manifold structure, etc.) in order to be able to say something new and non-trivial about the problem at hand.
rian 14y ago
awesome post! one suggestion: following your explanation it seems like the type constructors are more responsible for determining whether it is sum or product type instead of the data constructors. this tripped me up when i was trying to figure out why function types didn't have a size of a * b, and instead b^a. then i remembered that Add takes the same amount of arguments as Mul in the type constructor despite it being a sum type. i would hint more that what determines the size of a type isn't the type constructor but more the different data constructors, e.g.: data T a b = Foo a | Bar a b | Baz b | Qux (a -> b) <=> T = a + a*b + b + b^a i'm already anticipating your recursive type post :) data Rec a b = One a | Two a b (Rec a b) | Three b <=> T = a + a * b * T + b T - T * a * b = a + b T * (1 - a * b) = a + b T = (a + b) / (1 - a * b) ... in haskell's ADT's how do you get the inverses of a type? then we could solve for the size of the recursive type Rec a b.
opminion 14y ago
Ok, so type == cardinality, roughly speaking, is my understanding of the article when read with the pure mathematics hat on. Now that's interesting. Cardinality was the first topic in my Calculus course, and rather fascinating as a mind opener when it got to infinites.

116 points by crntaylor 14y ago

mind blowing, this is just beautiful :)

If you want to see how crazy this can get, know that you can actually take the derivative of a type (with respect to another type), and this yields useful information. See McBride's paper http://strictlypositive.org/diff.pdf http://strictlypositive.org/diff.pdf , or this guy who is discovering it by himself: http://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work http://stackoverflow.com/questions/9190352/abusing-the-algeb...

cwzwarich 14y ago
This interpretation of the derivative of a formal power series was known in combinatorics long before people were studying algebraic data types in programming, so I am surprised that McBride presents it as novel.
crntaylor 14y ago
"This guy who is discovering it by himself" is me (the OP) about a year ago! Derivatives of types to come in part II or III (or just watch the talk on YouTube: http://www.youtube.com/watch?v=YScIPA8RbVE http://www.youtube.com/watch?v=YScIPA8RbVE)
kd0amg 14y ago
Also reminds me of http://www.cs.indiana.edu/~sabry/papers/rational.pdf http://www.cs.indiana.edu/~sabry/papers/rational.pdf

batterseapower 14y ago

Pedants would add that the analogy with number of inhabitants is all a little screwed up in Haskell since bottom is an implicit inhabitant of all data types, which means that e.g. Either Void () has a different number of inhabitants than () and so they cannot strictly speaking be made isomorphic. Strict languages can sidestep this problem to an extent but still end up with "wrong" numbers of inhabitants for e.g. T -> (), since (\_ -> ()) is different from (\_ -> undefined). So the only guys living in pure algebraic bliss are the total functional programmers like the Agda aficionados.

crntaylor 14y ago
Yup. I deliberately ignored ⊥ to simplify the presentation (and I make no apologies for doing so!) There are a couple of posts by Dan Piponi where he explores how to count inhabitants of types when you properly account for ⊥: http://blog.sigfpe.com/2008/02/how-many-functions-are-there-from-to.html He does it by counting the number of functions () -> () (where () is of course inhabited by both () and ⊥), and concludes that the number of functions () -> () depends on the semantics of the language: 1 in a total language (like Agda) or in mathematics. 3 in a lazy language (like Haskell) when working completely lazily. 4 in Haskell, when using seq to enforce strictness. 3 in a strict language (like ML). He then goes on to analyse the relationship between point-set topology and computability, showing that the set of computable functions is in a 1-1 correspondence to the set of continuous functions, under the appropriate topology: http://blog.sigfpe.com/2008/01/what-does-topology-have-to-do-with.html http://blog.sigfpe.com/2008/02/what-is-topology.html http://blog.sigfpe.com/2008/03/what-does-topology-have-to-do-with.html Fascinating stuff - but you can see why I decided not to talk about it! Edit: Aha, I just realized who you are, and that we've met before..!
jonsterling 14y ago
True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom. And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type. So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing. For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.
dons 14y ago
http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publications/fast+loose.pdf http://www.comlab.ox.ac.uk/oucl/work/jeremy.gibbons/publicat... Fast and loose reasoning is morally correct.

spacemanaki 14y ago

Ok, pardon my ignorance, but I'm curious if anyone can comment on how this does or doesn't relate to the Curry-Howard correspondence ? The very limited amount of introductory type theory that I've read (mostly Benjamin Pierce's TAPL and Software Foundations) seems to treat Curry-Howard as a deep and fundamental cornerstone, but the only places I've seen the algebraic properties of types explored is in blog posts (http://blog.lab49.com/archives/3011 http://blog.lab49.com/archives/3011). Is there some connection I just haven't figured out yet due to mathematical immaturity? I'm struggling to see the relationship between types as sums, products and exponents, and types as conjunction, disjunction and implication.

jonsterling 14y ago
One way to understand it is to think of the “type” side of things (sums, products, exponents) as the sort of things that one needs in order to prove the “propositional” side of things (disjunction, conjunction, implication). So, a term of a sum type will serve as a proof for the corresponding disjunction proposition, and so forth. As to how the number of terms in a given type follows in CH, it's just the number of possible proofs for the corresponding proposition.
tel 14y ago
The answer you're looking for is in category theory. For a long time people ad hoc recognized that "products" and "sums" exist in many different domains, but there wasn't a universal method to construct them. Category theory does just that by treating all of these things as special kinds of categories and reading off universal properties which link rings, algebraic data types, logic, sets, topological spaces, etc. etc.

pilgrim689 14y ago

I'm a beginner Haskeller and I'm really enjoying this blog so far. After reading through a few tutorials, it's refreshing to get some theoretical background to it all. It helps make the language more intuitive, even if it's not teaching concrete uses of the theory. Subscribed!

MBlume 14y ago
Thank you for causing me to notice that the last two haskell posts I really enjoyed were on the same blog. Also subscribed!

guygurari 14y ago

So the algebra of data types, as described, is simply the algebra of natural numbers. I guess this can't be the whole story because it does not describe types which can get an infinite number of values. But still I wonder, what is the practical advantage of using this simple mathematical structure? What does it buy us? Not trying to be snarky, I just don't see the point.

crntaylor 14y ago
Indeed, it's not the whole story. Infinite types and recursive types will come along in part 2! As to the practical advantage - does there have to be one? Isn't the fact that it's intellectually gratifying enough? If you insist, though - I sometimes see the kind of laws I presented used in actual Haskell code. For example, in the Data.Lens package[0] you can consider a lens on a a structure of type a to be composed of a getter and a setter of values of type b data Lens a b = Lens (a -> b, a -> b -> a) which is refactored, using the law (a -> b, a -> c) == a -> (b,c), to look like data Lens a b = Lens (a -> (b, b -> a)) which allows for a more efficient 'modify' operation. It also allows you to notice that lenses are related to the 'Store' comonad[1]: data Store b a = Store (b, b -> a) data Lens a b = Lens (a -> Store b a) on which a lot of the Data.Lens internals are based. [0] https://github.com/ekmett/lens https://github.com/ekmett/lens [1] http://stackoverflow.com/questions/8766246/what-is-the-store-comonad http://stackoverflow.com/questions/8766246/what-is-the-store...
- guygurari 14y ago
  Thanks for explaining and for the examples. I would like to clarify that by 'practical advantage' I do not mean 'how does this help us write a web app' (although that would be nice), I mean 'how does this help us better understand programming'. In my experience, if you find that a problem admits a mathematical structure, but the structure is very simple, then often the structure does not lead to interesting insights -- it is just a form of taxonomy. This happens for example in my field (theoretical physics), where some objects can be described in fancy ways using category theory. These descriptions do not lead to any practical results, like discovering new mathematical properties of the objects involved. Personally I do not find these descriptions gratifying because, again, they are just taxonomy. There usually needs to be some minimal amount of mathematical structure (like group structure, manifold structure, etc.) in order to be able to say something new and non-trivial about the problem at hand.

rian 14y ago

awesome post! one suggestion: following your explanation it seems like the type constructors are more responsible for determining whether it is sum or product type instead of the data constructors. this tripped me up when i was trying to figure out why function types didn't have a size of a * b, and instead b^a. then i remembered that Add takes the same amount of arguments as Mul in the type constructor despite it being a sum type. i would hint more that what determines the size of a type isn't the type constructor but more the different data constructors, e.g.: data T a b = Foo a | Bar a b | Baz b | Qux (a -> b) <=> T = a + a*b + b + b^a i'm already anticipating your recursive type post :) data Rec a b = One a | Two a b (Rec a b) | Three b <=> T = a + a * b * T + b T - T * a * b = a + b T * (1 - a * b) = a + b T = (a + b) / (1 - a * b) ... in haskell's ADT's how do you get the inverses of a type? then we could solve for the size of the recursive type Rec a b.

opminion 14y ago

Ok, so type == cardinality, roughly speaking, is my understanding of the article when read with the pure mathematics hat on. Now that's interesting. Cardinality was the first topic in my Calculus course, and rather fascinating as a mind opener when it got to infinites.