• Bool and Pair are dual!

    Right, so. I’ve “known” for a while that sum types (enums) and product types (structs) are dual in a precise sense. I even kind of intuitively understood what that “precise sense” is. But this example was particularly visceral.

    Here’s your bog-standard Church encoding of booleans:

    For example, reduces to , like you’d expect.

    And here’s your Church encoding of pairs:

    Wait, why do those inner lambdas in fst and snd look so familiar? And wait, isn’t pair just if with its arguments rearranged?

    …Oh my god.

  • This is a test

    ‘Ello everyone. I’m testing my new blog, server, etc. right now. Time will tell whether this post sticks around in the long term (it probably won’t), but for now, excuse the dust.

    (If a blogger publishes a post and nobody reads it, was it ever really published?)

    MathJax:

    Syntax highlighting:

    def parabola(a, b, c):
      def inner(x):
        return c + x*(b + x*a)
      return inner