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.<p>See McBride's paper <a href="http://strictlypositive.org/diff.pdf" rel="nofollow">http://strictlypositive.org/diff.pdf</a> , or this guy who is discovering it by himself: <a href="http://stackoverflow.com/questions/9190352/abusing-the-algebra-of-algebraic-data-types-why-does-this-work" rel="nofollow">http://stackoverflow.com/questions/9190352/abusing-the-algeb...</a>
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.<p>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).<p>So the only guys living in pure algebraic bliss are the total functional programmers like the Agda aficionados.
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 (<a href="http://blog.lab49.com/archives/3011" rel="nofollow">http://blog.lab49.com/archives/3011</a>).<p>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.
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!
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.<p>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.
awesome post! one suggestion:<p>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.:<p><pre><code> data T a b = Foo a | Bar a b | Baz b | Qux (a -> b) <=> T = a + a*b + b + b^a
</code></pre>
i'm already anticipating your recursive type post :)<p><pre><code> 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)
</code></pre>
... 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.
Ok, so type == cardinality, roughly speaking, is my understanding of the article when read with the pure mathematics hat on.<p>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.