{"id":3531,"date":"2018-01-17T11:00:49","date_gmt":"2018-01-17T16:00:49","guid":{"rendered":"http:\/\/www.goodmath.org\/blog\/?p=3531"},"modified":"2018-01-17T11:00:49","modified_gmt":"2018-01-17T16:00:49","slug":"inference-with-sets-in-type-theory","status":"publish","type":"post","link":"http:\/\/www.goodmath.org\/blog\/2018\/01\/17\/inference-with-sets-in-type-theory\/","title":{"rendered":"Inference with Sets in Type Theory"},"content":{"rendered":"

It’s been quite a while since I did any meaningful writing on type theory. I spent a lot of time introducing the basic concepts, and trying to explain the intuition behind them. I also spent some time describing what I think of as the platform: stuff like arity theory, which we need for talking about type construction. But once we move beyond the basic concepts, I ran into a bit of a barrier – no so much in understanding type theory, but in finding ways of presenting it that will be approacha ble.<\/p>\n

I’ve been struggling to figure out how to move forward in my exploration of type theory. The logical next step is working through the basics of intuitionistic logic with type theory semantics. The problem is, that’s pretty dry material. I’ve tried to put together a couple of approaches that skip over this, but it’s really necessary.<\/p>\n

For someone like me, coming from a programming language background, type theory really hits its stride when we look at type systems and particularly type inference. But you can’t understand type inference without understanding the basic logic. In fact, you can’t describe the algorithm for type inference without referencing the basic inference rules of the underlying logic. Type inference is nothing but building type theoretic proofs based on a program.<\/p>\n

So here we are: we need to spend some time looking at the basic logic of type theory. We’ve looked at the basic concepts that underlie the syntax and semantics, so what we need to do next is learn the basic rules that we use to build logical statements in the realm of type theory. (If you’re interested in more detail, this is material from chapter 5 of “Programming in Martin-Löof’s Type Theory”<\/a>, which is the text I’m using to learn this material.)<\/p>\n

Martin Löoff’s type theory is a standard intuitionistic predicate logic, so we’ll go through the rules using standard sequent notation. Each rule is a sequence which looks sort-of like a long fraction. The “numerator” section is a collection of things which we already know are true; the “denominator” is something that we can infer given those truths. Each statement has the form A[\\Gamma], where A is a statement, and B is a set of assumptions. For example, F(a) [a \\in A, \\Delta] means that F(a) is true, provided we’re in a context that includes a \\in A.<\/p>\n

Personally, I find that this stuff feels very abstract until you take the logical statements, and interpret them in terms of programming. So throughout this post, I’ll do that for each of the rules.<\/p>\n

With that introduction out of the way, let’s dive in to the first set of rules.<\/p>\n

Simple Introductions <\/h3>\n

We’ll start off with a couple of really easy rules, which allow us to introduce a variable given a type, or a type given a variable.<\/p>\n

Introducing Elements<\/h4>\n

\\frac{A \\,\\text{type}}{a \\in A \\,[a \\in A]}<\/center><\/p>\n

This is an easy one. It says that if we know that A is a type, then we can introduce the statement that a \\in A, and add that as an assumption in our context. What this means is also simple: since our definition of type says that it’s only a type if it has an element, then if we know that A is a type, we know that there must be an element of A, and so we can write statements using it.<\/p>\n

If you think of this in programming terms, the statement A \\text{type} is saying that A is a type. To be a valid type, there must be at least one value that belongs to the type. So you’re allowed to introduce a variable that can be assigned a value of the type.<\/p>\n

Introducing Propositions as Types<\/h4>\n

\\frac{a \\in A \\, []}{A \\, \\text{true}}<\/center><\/p>\n

This is almost the mirror image of the previous. A type and a true proposition are the same thing in our type theory: a proposition is just a type, which is a set with at least one member. So if we know that there’s a member of the set A, then A is both a type and a true proposition. <\/p>\n

Equality Rules<\/h3>\n

We start with the three basic rules of equality: equality is reflexive, symmetric, and transitive.<\/p>\n

Reflexivity<\/h4>\n

\\frac{a \\in A}{a = a \\in A}<\/center><\/p>\n

\\frac{A \\, \\text{type}}{A = A}<\/center><\/p>\n

If a is an element of a type A, then a is equal to itself in type A; and if A is a type, then A is equal to itself. <\/p>\n

The only confusing thing about this is just that when we talk about an object in a type, we make reference to the type that it’s a part of. This makes sense if you think in terms of programming: you need to declare the type of your variables. “3: Int” doesn’t necessarily mean the same object as “3: Real”; you need the type to disambiguate the statement. So within type theory, we always talk about values with reference to the type that they’re a part of. <\/p>\n

Symmetry<\/h4>\n

\\frac{a = b \\in A}{b = a \\in A}<\/center><\/p>\n

\\frac{A = B}{B = A}<\/center><\/p>\n

No surprises here – standard symmetry.<\/p>\n

Transitivity<\/h4>\n

\\frac{a = b \\in A \\quad b = c \\in A}{a = c \\in A}<\/center><\/p>\n

\\frac{A = B \\quad B = C}{A = C}<\/center><\/p>\n

Type Equality<\/h4>\n

\\frac{a \\in A \\quad A = B}{a \\in B}<\/center><\/p>\n

\\frac{a = b \\in A \\quad A = B}{a = b \\in B}<\/center><\/p>\n

These are pretty simple, and follow from the basic equality rules. If we know that a is a member of the type A, and we know that the type A equals the type B, then obviously a is also a member of B. Along the same lines, if we know that a=b in type A, and A equals B, then a=b in the type B. <\/p>\n

Substitution Rules<\/h3>\n

We’ve got some basic rules about how to formulate some simple meaningful statements in the logic of our type theory. We still can’t do any interesting reasoning; we haven’t built up enough inference rules. In particular, we’ve only been looking at simple, atomic statements using parameterless predicates.<\/p>\n

We can use those basic rules to start building upwards, to get to parametric statements, by using substitution rules that allow us to take a parametric statement and reason with it using the non-parametric rules we talked about above.<\/p>\n

For example, a parametric statement can be something like C(x) \\, \\text{type} [x \\in A], which says that applying C to a value x which is a member of type A produces a value which is a type. We can use that to produce new inference rules like the ones below.<\/p>\n

\\frac{C(x) \\, \\text{type} [x \\in A] \\quad a \\in A}{C(a) \\, \\text{type}}<\/center><\/p>\n

This says that if we know that given a of type A, C will produce a type; and we know that the value a is of type A, then C(a) will be a type. In logical terms, it’s pretty straightforward; in programming terms it’s even clearer: if C is a function on type A, and we pass it a value of type A, it will produce a result. In other words, C(a) is defined for all values of type A.<\/p>\n

\\frac{C(x) \\, \\text{type}[x \\in A] \\quad a = b \\in A}{C(a) = C(b)}<\/center><\/p>\n

This is even simpler: if C is a function on type A, then given two values that are equal in type A, C will produce the same result for those values.<\/p>\n

Of course, I’m lying a bit. In this stuff, C isn’t really a function. It’s a logical statement; C(x) isn’t quite a function. It’s a logical stamement which includes the symbol x; when we say C(a), what we mean is the logical statement C, with the object a substituted for the symbol x. But I think the programming metaphors help clarify what it means.<\/p>\n

Using those two, we can generate more:<\/p>\n

\\frac{c(x) \\in C(x) [x \\in A] \\quad a \\in A}{c(a) \\in C(A)}<\/center><\/p>\n

This one becomes interesting. C(x) is a proposition which is parametric in x. Then c(x) is a proof-element<\/em>: it’s an instance of C(x) which proves that C(X) is a type, and we can see c as a computation which, given an element of a produces a instance of C. Then what this judgement says is that given an instance a of type A, we know that c(a) is an instance of type C(a). This will become very important later on, when we really get in to type inference and quantification and parametric types.<\/p>\n

\\frac{c(x) \\in C(x) [x \\in A] \\quad a = b}{c(a)=c(b)\\in C(a)}<\/center><\/p>\n

This is just a straightforward application of equality to proof objects.<\/p>\n

There’s more of these kinds of rules, but I’m going to stop here. My goal isn’t to get you to know every single judgement in the intuitionistic logic of type theory, but to give you a sense of what they mean. <\/p>\n

That brings us to the end of the basic inference rules. The next things we’ll need to cover are ways of constructing new types or types from existing ones. The two main tools for that are enumeration types (basically, types consisting of a group of ordered values), and cartesian products of multiple types. With those, we’ll be able to find ways of constructing most of the types we’ll want to use in programming languages.<\/p>\n","protected":false},"excerpt":{"rendered":"

It’s been quite a while since I did any meaningful writing on type theory. I spent a lot of time introducing the basic concepts, and trying to explain the intuition behind them. I also spent some time describing what I think of as the platform: stuff like arity theory, which we need for talking about […]<\/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-3531","post","type-post","status-publish","format-standard","hentry","category-type-theory"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"","jetpack_shortlink":"https:\/\/wp.me\/p4lzZS-UX","jetpack_sharing_enabled":true,"jetpack_likes_enabled":true,"_links":{"self":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3531","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=3531"}],"version-history":[{"count":18,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3531\/revisions"}],"predecessor-version":[{"id":3549,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/posts\/3531\/revisions\/3549"}],"wp:attachment":[{"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/media?parent=3531"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/categories?post=3531"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/www.goodmath.org\/blog\/wp-json\/wp\/v2\/tags?post=3531"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}