Abusing the algebra of algebraic data types – why does this work?

This page summarizes the projects mentioned and recommended in the original post on news.ycombinator.com

Our great sponsors
  • WorkOS - The modern identity platform for B2B SaaS
  • InfluxDB - Power Real-Time Data Analytics at Scale
  • SaaSHub - Software Alternatives and Reviews
  • coq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.

    As someone who has graduate level math education and about 25 years working as a professional programmer, I emphatically disagree.

    A type system is itself a programming language. If it is going to implement complex enough logic, it will be Turing complete. It does not magically become clearer simply because it ideas have been expressed in a type system. For an amusing demonstration, read through https://aphyr.com/posts/342-typing-the-technical-interview. That is a working program that solves the 8 queens problem entirely in Haskell's type system.

    And the type systems that you are used to are simpler in part because they are NOT Turing complete. This limits what you can say in them. In this case, for example, the author was unable to express higher derivatives as types.

    Now perhaps your desire is for unambiguous machine-checkable logic? If so then I highly recommend learning something like https://coq.inria.fr/. It is a worthwhile enterprise, and there are serious mathematicians who say that it, or something like it, should be implemented for all of math. However one of the objections to it is that it is harder to express and understand yourself in such systems. So unambiguous machine-checkability is a win, but not necessarily the one you thought it was.

    And then we come to the real issue. Are you optimizing for use, or for the person who doesn't understand the subject? It is literally impossible to think about complex things without a concise notation. The actual notation that we have has a lot of history and rough spots. But verbosity impedes comprehension. So what makes life easy for the novice and expert are exactly opposite. But most of the use of the material is by experts, who are also who the notation is for. Indeed the notation helps so much that within a course or two it has paid off - learning the same ideas WITHOUT the notation would have been harder than learning both notation and ideas. The notation merely creates a first obvious barrier. But it is far less of a barrier than the ideas. And it seriously is helpful in mastering the ideas.

    I know you don't believe me. You've told others that it is about what works best for you. But with all due respect, you can't have any idea what actually works best until you've actually mastered a sufficient amount of the subject. Until then you are best off believing people who HAVE mastered the subject, and have spent sufficient time teaching and tutoring to know where the real barriers to understanding are for students. And everyone I know in that boat, including me, says that the notation helps more than it hurts.

  • WorkOS

    The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.

NOTE: The number of mentions on this list indicates mentions on common posts plus user suggested alternatives. Hence, a higher number means a more popular project.

Suggest a related project

Related posts