Reddit reviews Principia Mathematica - Volume One

> You seem to be responding as if I'd made some claim that dynamically typed programs are free of the sources of complexity I identify. They most certainly are not.

I would argue that that's implicit in your having used sum types as one of your examples. So we can strike that one from the list, then, since sum types parallel equally complex structures in dynamically typed languages.

> Were it not a set you couldn't have exhaustiveness checks.

You can think of a sum type as a set if you like, and if exhaustiveness checks were the only feature of sum types, obviously, you would have to. They aren't, and you don't. Again, I can't recall the last time I asked the compiler to turn warnings (including exhaustiveness checks) into errors, which is what it would take if I wanted to treat lack of exhaustiveness as a "type error."

> You couldn't have demonstrated better the problem with type systems advocacy, as seen by those who have to deliver programs that work to the satisfaction of the world outside the program.

Two things:

1. You seem to be arguing that somehow, not having product types would be a superior way to "deliver programs that work to the satisfaction of the world outside the program" than having them. That's ridiculous, if for no other reason than that lack of any structure at all isn't an improvement on imperfect structure.
   
2. By implication, those of us who advocate type systems don't have to deliver programs that work to the satisfaction of the world outside the program. To put it gently, that's not an argument you want to make, and your condescension is wildly misplaced, albeit typical of the Lisp community.
   
   > "Mathematics may be defined as the subject in which we never know what we are talking about, nor whether what we are saying is true." - Bertrand Russell
   
   Yes, Betrand Russell, co-author of the Principia Mathematica, which defined a logic that Kurt Gödel later proved had to be either inconsistent or incomplete. Thankfully the development of logic didn't end there—it's tempting to say it started there—and we have powerful, consistent logics like the Calculus of Inductive Constructions in the Coq proof assistant to use, if we want to go that far. But usually, the very good type systems of languages like Scala, OCaml, or Haskell are plenty good enough.