>One question you might have is “what the heck does it mean for a type to be correct?” Good question! It means your type should be as polymorphic as possible.

>One question you might have is “what the heck does it mean for a type to be correct?” Good question! It means your type should be as polymorphic as possible. There's a mathematical sense in which this is correct, but I disagree for practical software. Yes, there's only one function of type (forall a. a -> a), so you can't screw it up if you have a type checker, while you can easily screw up a function of type (BizLogicType -> BizLogicType) since there are going to be many of those. But when reading code, the most polymorphic version of a function struggles from the same problem that using "x" as a variable name does. It's the type level version of the difference between ( x = f(g) ) and ( numBooks = countBooks(library) ).