Hacker News new | past | comments | ask | show | jobs | submit login

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.




Join us for AI Startup School this June 16-17 in San Francisco!

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: