{"id":3113,"date":"2015-02-04T16:33:17","date_gmt":"2015-02-04T21:33:17","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3113"},"modified":"2015-02-04T16:33:17","modified_gmt":"2015-02-04T21:33:17","slug":"the-program-is-the-proof-propositions-in-type-theory","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2015\/02\/04\/the-program-is-the-proof-propositions-in-type-theory\/","title":{"rendered":"The Program is the Proof: Propositions in Type Theory"},"content":{"rendered":"

As usual, I’m going in several different directions. I’m going to continue doing data structure posts, but at the same time I also want to get back to the type theory stuff that I was writing about before I put the blog on hiatus.<\/p>\n

So let’s get back to a bit of Martin-Loff type theory! (The stuff I’m writing about today corresponds, roughly, to chapter 2 of the Nordstrom\/Petersson\/Smith text.)<\/p>\n

One of the key ideas of Martin-Loff’s type theory is that a logical statement is exactly the same thing as a specification of a computation. When you define a predicate like “Even”, the definition specifies both the set of numbers that satisfy the predicate, and the computation that tests a number for membership in the set of even numbers. If you haven’t provided enough information to fully specify the computation, then in Martin-Loff type theory, you haven’t defined a predicate or a set.<\/p>\n

When you say “2 is even”, what you’re really saying in terms of the type theory is that “The computation for ‘even(2)’ will succeed”. The computation and the logical statement are the same thing<\/em>.<\/p>\n

In functional programming, we like to say that the program is the proof. Martin-Loff type theory is where that came from – and today we’re going to take a first look in detail at exactly what it means. In the world of type theory, the program is the proof, and the proof doesn’t exist without the program.<\/p>\n

This creates an interesting set of equivalent interpretations. When you see a statement like “x : T” (or x \\in T), that could be interpreted in the following ways, all of which are really equivalent in type theory.<\/p>\n

    \n
  1. Set theoretic<\/em>: x is a member<\/em> of the set<\/em> T.<\/li>\n
  2. Intuitionistic<\/em>: x is a proof object<\/em> for the proposition<\/em> T.<\/li>\n
  3. Computational<\/em>: x is a program<\/em> that satisfies the specification<\/em> T.<\/li>\n
  4. Abstract<\/em>: x is a solution<\/em> for the problem<\/em> T.<\/li>\n<\/ol>\n

    In the rest of this post, I’m going to focus on those four interpretations, and explain how each of them makes sense in this version of type theory.<\/p>\n

    The set theoretic interpretation is obvious – as the name suggests, it’s nothing but what we all learned from basic set theory. An object is a member of a set – which means, from set theory, that the object satisfies some predicate in first order predicate logic – because that’s what it means to be a member of a set.<\/p>\n

    The intuitionistic interpretation is almost the same as the set theoretic, but rewritten for intuitionistic logic. In intuitionistic logic, the predicate over the set is written as a proposition T, and if we know that x is a member of the set T, then that means that we have a proof that x demonstrates that T is true.<\/p>\n

    The computational interpretation takes the intuitionistic one, and rephrases it in computational terms. A logical proposition, rendered into a computational setting, is just a specification of a program; and a proof of the proposition is a program that satisfies the specification.<\/p>\n

    Finally, the abstract interpretation just rephrases the computational one into terms that aren’t tied to a computing device. A predicate is a problem that needs to be solved; anything that provides a solution to the problem is demonstrating a member of the set.<\/p>\n

    The key takeaway though is the basic idea here of what a type<\/em> is. What we’re talking about as a type here is something that goes far beyond any programming language’s idea of what a type is. In intuitionistic type theory, a type is a specification of a computation<\/em>. If we had this in a real language, that would mean that any program that typechecked would be guaranteed<\/em> to work: asserting that x has type T means, precisely, that x is a computation that matches the specification!<\/p>\n

    (Of course, that’s not the panacea that you might think the first time you hear that. The catch is simple: the type is a specification of the computation. That means that just writing a type is a form of programming! And that means that your type descriptions are going to have bugs. But we’ll come back to that in a much later post.)<\/p>\n

    What type theory is doing is taking something like set theory, and re-rendering it entirely in a computational world. It still has a mapping from the computations to the abstract concepts that we use when we’re thinking, but if we can talk about those abstract concepts in type theory, we’ll always do it by mapping them into some kind of computation. <\/p>\n

    In type theory, we’re not dealing in a world of pure mathematical objects that exist if we can describe them; instead, we’re building a world where everything is at least theoretically computable. That might seem constraining, but every proof already corresponds to a computation of some sort; the only additional constraint here is that we can’t play tricks like the axiom of choice, where we can “prove” the existence of some unattainable, intangible, nonsensical object.<\/p>\n

    To make that work, we’re going to take all of the construct that we’re used to seeing in intuitionistic logic, and give them a meaning in terms of computations.<\/p>\n

    For example, in set theory, we can have a statement A \\supset B – meaning that A is a superset of B, that every element of B is also necessarity an element of A. In type theory, since A and B are specifications of computations, that means that a member (or proof) of A \\supset B is a computation that given a proof of A, generates a proof of B – in short, that A implies B.<\/p>\n

    Now, suppose that we want to prove A \\supset A. How could we do that? We need a program that given a proof of A generates a proof of A. That is, we need an implementation of the identity function: \\lambda a . a. <\/p>\n

    In fact, using the computation interpretation of things, we can interpret A \\supset B as being the type of a function that takes an instance of a, and generates an instance of b – that is, that if f : (A \\supset B), then f is a function from an instance of A to an instance of B!<\/p>\n

    The only trick to that is understanding that in type theory, saying that a is an element of A means that a is a proof of A. Using the same interpretation, that means that f: A \\supset B means that f is a proof of A \\supset B – which means the same thing as saying that given an example of an element of A (a proof of A), f will produce an element of B (a proof of B). The statement A \\supset B is exactly the same thing as the logical implication A \\rightarrow B, which is exactly the same thing as the type<\/em> of a function from A to B.<\/p>\n\n

    <\/p>\n

    Notes on sources: I’m working from two main references in this series of posts, both of which are available in PDF form online.<\/p>\n

      \n
    1. “Programming in Martin-Lof’s Type Theory”, by Nordstrom, Petersson, and Smith, which you can download here<\/a>.<\/li>\n
    2. “Type Theory and Functional Programming” by Simon Thompson (available here<\/a>).<\/li>\n<\/ol>\n

      In addition, I first learned a lot of this from reading some papers by Phil Wadler and Simon Peyton Jones. The exactly references but the exact references to those are long-lost in the shadows of my memory. But any of their papers are well-worth reading, so just read them all!)<\/p>\n

      <\/em><\/p>\n","protected":false},"excerpt":{"rendered":"

      As usual, I’m going in several different directions. I’m going to continue doing data structure posts, but at the same time I also want to get back to the type theory stuff that I was writing about before I put the blog on hiatus. So let’s get back to a bit of Martin-Loff type theory! […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","default_image_id":0,"font":"","enabled":false},"version":2}},"categories":[292],"tags":[],"class_list":["post-3113","post","type-post","status-publish","format-standard","hentry","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-Od","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3113","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/comments?post=3113"}],"version-history":[{"count":2,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3113\/revisions"}],"predecessor-version":[{"id":3115,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3113\/revisions\/3115"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3113"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3113"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3113"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}