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).
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.
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.
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.
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.