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

The idea that types are the same because the cardinalities of their sets of values are the same is weird. So my type for the days of the week is "equal" to my enumeration of the Seven Dwarves, and the sum of Maybe Bool and Bool->Bool? How is that a useful definition?

They aren’t the same, they’re isomorphic—there exists some isomorphism between them, which is to say a bijective homomorphism, which is to say a one-to-one mapping between two algebraic structures, which is to say types. Category theory is too damn abstract.

In any case, having isomorphic structures means that any transformation you apply to one can be applied to the other by way of a particular isomorphism. There is a “next” day of the week, in the same way that there is a “next” Dwarf by order of introduction[1], in the same way that there is a “next” value in this partial ordering I just made up for (Either (Maybe Bool) (Bool -> Bool)) which you can’t program in Haskell:

Left Nothing < Left (Just False) < Left (Just True) < Right (const False) < Right id < Right not < Right (const True)

[1]: Doc, Bashful, Sleepy, Sneezy, Happy, Dopey, and Grumpy.

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact