Truth in Type Theory

Now, we’re getting to the heart of type theory: judgements. Judgements are the basic logical statements that we want to be able to prove about computations in type theory. There’s a basic set of judgements that we want to be able to make.

I keep harping on this, but it’s the heart of type theory: type theory is all about understanding logical statements as specifications of computations. Or, more precisely, in computer science terms, they’re about understanding true logical statements as halting computations.

In this post, we’ll see the ultimate definition of truth in type theory: every logical proposition is a set, and the proposition is true if the set has any members. A non-halting computation is a false statement – because you can never get it to resolve an expression to a canonical value.

So remember as we go through this: judgements are based on the idea of logical statements as specifications of computations. So when we talk about a predicate P, we’re using its interpretation as a specification of a computation. When we look at an expression 3+5, we understand it not as a piece of notation that describes the number 8, but as a description of a computation that adds 3 to 5. “3+5” not the same computation as “2*4” or “2+2+2+2”, but as we’ll see, they’re equal because they evaluate to the same thing – that is, they each perform a computation that results in the same canonical value – the number 8.

In this post, we’re going to focus on a collection of canonical atomic judgement types:

A \text{set}
This judgement says that A is a set.
A = B
A and Bare equal sets.
a \in A
a is an element of the set A
a_1 == a_2 \in A
a_1 and a_2 are equal members of the set A.
A is a proposition.
The proposition A is true.

The definition of the meanings of judgements is, necessarily, mutually recursive, so we’ll have to go through all of them before any of them is complete.

An object A is a Set
When I say that A is a set in type theory, that means that:

  • I know the rules for how to form the canonical expressions for the set;
  • I’ve got an equivalence relation that says when two canonical members of the set are equal.
Two Sets are Equal

When I say that A and B are equal sets, that means:

  • A and B are both sets.
  • If a is a canonical member of A, then a is also a canonical member of B, and vice versa.
  • If a and b are canonical members of A, and they’re also equal in A, then a and b are also equal canonical members of B (and vice versa).

The only tricky thing about the definition of this judgement is the fact that it defines equality is a property of a set, not of the elements of the set. By this definition, tt’s possible for two expressions to be members of two different sets, and to be equal in one, but not equal in the other. (We’ll see in a bit that this possibility gets eliminated, but this stage of the definition leaves it open!)

An object is a member of a set
When I say a \in A, that means that if I evaluate a, the result will be a canonical member of A.
Two members of a set are equal
If a \in A and b \in A and a = b, that means when if you evaluate a, you’ll get a canonical expression a; and when you evaluate b, you’ll get a canonical expression b. For a == b to be true, then a, that is, the canonical expressions resulting from their evaluation must also be equal.

This nails down the problem back in set equivalence: since membership equivalence is defined in terms of evaluation as canonical values, and every expression evaluates to exactly one canonical expression (that’s the definition of canonical!), then if two objects are equal in a set, they’re equal in all sets that they’re members of.

An object A is a proposition
Here’s where type theory really starts to depart from the kind of math that we’re used to. In type theory, a proposition is a set. That’s it: to be a proposition, A has to be a set.
The proposition A is true
And the real meat of everything so far: if we have a proposition A, and A is true, what that means is that a has at least one element. If a proposition is a non-empty set, then it’s true. If it’s empty, it’s false.

Truth in type theory really comes down to membership in a set. This is, subtly, different from the predicate logic that we’re familiar with. In predicate logic, a quantified proposition can, ultimately, be reduced to a set of values, but it’s entirely reasonable for that set to be empty. I can, for example, write a logical statement that “All dogs with IQs greater that 180 will turn themselves into cats.” A set-based intepretation of that is the collection of objects for which it’s true. There aren’t any, because there aren’t any dogs with IQs greater than 180. It’s empty. But logically, in terms of predicate logic, I can still say that it’s “true”. In type theory, I can’t: to be true, the set has to have at least one value, and it doesn’t.

In the next post, we’ll take these atomic judgements, and start to expand them into the idea of hypothetical judgements. In the type-theory sense, that means statements require some other set of prior judgements before they can be judged. In perhaps more familiar terms, we’ll be looking at type theory’s equivalent of the contexts in classical sequent calculus – those funny little \Gammas that show up in all of the sequent rules.

Weekend Recipe: 3-cup chicken

This is a traditional chinese dish that my wife grew up eating in Taiwan. For some reason, she never told me about it, until she saw an article with a recipe in the NY Times. Of course, I can’t leave recipes alone; I always put my own spin on it. And the recipe in the article had some (in my opinion) glaring problems. For example, it called for cooking with sesame oil. Sesame oil is a seasoning, not a cooking oil. It’s got a very strong flavor, and it burns at stir-fry temperature, which makes any dish cooked in it taste absolutely awful. You cook in neutral oils with high smoke points, like peanut, canola, or soybean; and then you add a drop of sesame as part of the sauce, so that it’s moderated and doesn’t burn. Anyway, below is my version of the dish.

  • 2 pounds of chicken thighs, cut into bite-sized pieces.
  • About 8 large cloves of garlic, thickly sliced.
  • About a 1-inch section of fresh ginger, cut into disks.
  • 5 whole dried szechuan chili peppers (or more, if you like those lovely things!)
  • A good bunch of thai basil leaves, removed from the stems, but left whole. (About a cup, if it’s packed pretty tight. Don’t skimp – these are the best part of the dish!)
  • 4 scallions, thinly sliced, whites and greens separated.
  • 1/3 cup soy sauce.
  • 1/4 cup mirin
  • 1/2 cup sake
  • 1 tablespoon sugar
  • 1 teaspoon cornstarch, dissolved in water.
  • 1/4 teaspoon sesame oil (just a drop, for flavor).
  • Enough canola oil (or similarly bland, high-smoke-point cooking oil) to took – a couple of tablespoons at most.
  1. Get your wok smoking hot. Add enough oil to coat the bottom, and swirl it around.
  2. Add in half of the chicken, and cook until it’s nicely browned, then remove it. (It won’t be cooked all the way through yet, don’t worry!)
  3. Repeat with the other half of the chicken.
  4. Make sure there’s enough oil in the bottom of the wok, then toss in the garlic, ginger, chili peppers, and scallion whites. Stir fry them until the garlic starts to get just a little bit golden.
  5. Add the chicken back in, and add the soy, mirin, sake, and sugar. Get it boiling, and keep stirring things around until the chicken is cooked through.
  6. Add the basil and scallions, and keep stirring until the basil wilts, and the whole thing smells of that wonderful thai basic fragrance.
  7. Add the cornstarch and sesame oil, and cook until the sauce starts to thicken.
  8. Remove it from the heat, and serve on a bed of white rice, along with some simple stir-fried vegetables. (I used a batch of beautiful sugar-snap peas, quickly stir fried with just a bit of garlic, and a bit of soy sauce.)

A couple of notes on ingredients:

  • This is a dish where the soy sauce matters. Don’t use cheap generic american soy sauce; that stuff is just saltwater with food coloring. For some things, that’s actually OK. But in this dish, it’s the main flavor of the sauce, so it’s important to use something with a good flavor. Get a good quality chinese soy (I like Pearl River Bridge brand), or a good japanese shoyu.
  • For the sugar, if you’ve got turbinado (or even better, real chinese rock sugar), use that. If not, white sugar is Ok.
  • Definitely try to get thai basil. It’s very different from italian basil – the leaves are thinner (which makes them much easier to eat whole, as you do in this dish), and they’ve got a very different flavor – almost like Italian basic mixed with a bit of anise and a bit of menthol. It’s one of my favorite herbs, and it’s actually gotten pretty easy to find.
  • Szechuan peppers can be hard to find – you pretty much need to go to an Asian grocery. They’re worth it. They’ve got a very distinctive flavor, and I don’t know of any other dried pepper that works in a sauce like them. You don’t actually eat the peppers – the way you cook them, they actually burn a bit – but they bloom their flavor into the oil that you use to cook the rest of the dish, and that totally changes the sauce.

Canonical Expressions in Type Theory

Sorry for the gap in posts. I’ve been trying to post more regularly, and was just hitting a rhythm, when my son brought home a particularly vicious bug, and I got sick. I’ve spent the last couple of weeks being really, really sick, and then trying to get caught up at work. I’m mostly recovered, except for some lingering asthma, so I’m trying to get back to that twice-per-week posting schedule.

In the last couple of posts, we looked at Martin-Löf’s theory of expressions. The theory of expressions is purely syntactic: it’s a way of understanding the notation of expressions. Everything that we do in type theory will be written with expressions that follow the syntax, the arity, and the definitional equivalency rules of expression theory.

The next step is to start to understand the semantics of expressions. In type theory, when it comes to semantics, we’re interested in two things: evaluation and judgements. Evaluation is the process by which an expression is reduced to its simplest form. It’s something that we care about, but it’s not really a focus of type theory: type theory largely waves its hands in the air and says “we know how to do this”, and opts for normal-order evaluation. Judgements are where things get interesting.

Judgements are provable statements about expressions and the values that they represent. As software people, when we think about types and type theory, we’re usually thinking about type declarations: type declarations are judgements about the expressions that they apply to. When you write a type declaration in a programming language, what you’re doing is asserting the type theory judgement. When the compiler “type-checks” your program, what it’s doing in type theory terms is checking that your judgements are proven by your program.

For example, we’d like to be able to make the judgement A set – that is, that A is a set. In order to make the judgement that A is a set in type theory, we need to know two things:

  1. How are canonical instances of the set A formed?
  2. Given two canonical instances of A, how can we determine if they’re equal?

To understand those two properties, we need to take a step back. What is a canonical instance of a set?

If we think about how we use predicate logic, we’re always given some basic set of facts as a starting point. In type theory, the corresponding concept is a primitive constant. The primitive constants include base values and primitive functions. For example, if we’re working with lispish expressions, then cons(1, cons(2, nil)) is an expression, and cons, nil, 1 and 2 are primitive constants; cons is the head of the expression, and 1 and cons(2, nil) are the arguments.

A canonical expression is a saturated, closed expression whose head is a primitive constant.

The implications of this can be pretty surprising, because it means that a canonical expression can contain unevaluated arguments! The expression has to be saturated and closed – so its arguments can’t have unbound variables, or be missing parameters. But it can contain unevaluated subexpressions. For example, if we were working with Peano arithmetic in type theory, succ(2+3) is canonical, even though “2+3” hasn’t be evaluated.

In general, in type theory, the way that we evaluate an expression is called normal order evaluation – what programming language people call lazy evaluation: that’s evaluating from the outside in. Given a non-canonical expression, we evaluate from the outside in until we get to a canonical expression, and then we stop. A canonical expression is considered the result of a computation – so we can see succ(2+3) as a result!

A canonical expression is the evaluated form of an expression, but not the fully evaluated form. The fully evaluated form is when the expression and all of its saturated parts are fully evaluated. So in our previous example, the saturated part 2+3 wasn’t evaluated, so it’s not fully evaluated. To get it to be fully evaluated, we’d need to evaluate 2+3, giving us succ(5); then, since succ(5) is saturated, it’s evaluated to 6, which is the fully evaluated form of the expression.

Next post (coming monday!), we’ll use this new understanding of canonical expressions, and start looking at judgements, and what they mean. That’s when type theory starts getting really fun and interesting.

The Bad Logic of Good People Can’t be Sexists

One of my constant off-topic rants around here is about racism and sexism. This is going to be a nice little post that straddles the line. It’s one of those off-topic-ish rants about sexism in our society, but it’s built around a core of bad logic – so there is a tiny little bit of on-topicness.

We live in a culture that embodies a basic conflict. On one hand, racism and sexism are a deeply integrated part of our worldview. But on the other wand, we’ve come to believe that racism and sexism are bad. This puts us into an awkward situation. We don’t want to admit to saying or doing racist things. But there’s so much of it embedded in every facet of our society that it takes a lot of effort and awareness to even begin to avoid saying and doing racist things.

The problem there is that we can’t stop being racist/sexist until we admit that we are. We can’t stop doing sexist and racist things until we admit that we do sexist and racist things.

And here’s where we hit the logic piece. The problem is easiest to explain by looking at it in formal logical terms. We’ll look at it from the viewpoint of sexism, but the same argument applies for racism.

  1. We’ll say \text{Sexist}(x) to mean that “x” is sexist.
  2. We’ll say \text{Bad}(x) to mean that x is bad, and \text{Good}(x) to mean that x is good.
  3. We’ll have an axiom that bad and good are logical opposites: \text{Bad}(x) \Leftrightarrow \lnot \text{Good}(x).
  4. We’ll have another axiom that sexism is bad: \forall x: \text{Sexist}(x) \Rightarrow \text{Bad}(x).
  5. We’ll say \text{Does}(p, x) means that person p does an action x.

The key statement that I want to get to is: We believe that people who do bad things are bad people: \forall p, x: \text{Does}(p, x) \land \text{Bad}(x) \Rightarrow \text{Bad}(p).

That means that if you do something sexist, you are a bad person:

  • s is a sexist action: \text{Sexist}(s).
  • I do something sexist: \text{Does}(\textbf{markcc}, s).
  • By rule 5 above, that means that I am sexist.
  • If I am sexist, then by rule 4 above, I am bad.

We know that we aren’t bad people: I’m a good person, right? So we reject that conclusion. I’m not bad; therefore, I can’t be sexist, therefore whatever I did couldn’t have been sexist.

This looks shallow and silly on the surface. Surely mature adults, mature educated adults couldn’t be quite that foolish!

Now go read this.

If his crime was to use the phrase “boys with toys”, and that is your threshold for sexism worthy of some of the abusive responses above, then ok – stop reading now.

My problem is that I have known Shri for many years, and I don’t believe that he’s even remotely sexist. But in 2015 can one defend someone who’s been labeled sexist without a social media storm?

Are people open to the possibility that actually Kulkarni might be very honourable in his dealings with women?

In an interview a week or so ago, Professor Shri Kulkarni said something stupid and sexist. The author of that piece believes that Professor Kulkarni couldn’t have said something sexist, because he knows him, and he knows that he’s not sexist, because he’s a good guy who treats women well.

The thing is, that doesn’t matter. He messed up, and said something sexist. It’s not a big deal; we all do stupid things from time to time. He’s not a bad person because he said something sexist. He just messed up. People are, correctly, pointing out that he messed up: you can’t fix a problem until you acknowledge that it exists! When you say something stupid, you should expect to get called on it, and when you do, you should accept it, apologize, and move on with your life, using that experience to improve yourself, and not make the mistake again.

The thing about racism and sexism is that we’re immersed in it, day in and day out. It’s part of the background of our lives – it’s inescapable. Living in that society means means that we’ve all absorbed a lot of racism and exism without meaning to. We don’t have to like that, but it’s true. In order to make things better, we need to first acklowledge the reality of the world that we live in, and the influence that it has on us.

In mathematical terms, the problem is that good and bad, sexist and not sexist, are absolutes. When we render them into pure two-valued logic, we’re taking shades of gray, and turning them into black and white.

There are people who are profoundly sexist or racist, and that makes them bad people. Just look at the MRAs involved in Gamergate: they’re utterly disgusting human beings, and the thing that makes them so despicably awful is the awfulness of their sexism. Look at a KKKer, and you find a terrible person, and the thing that makes them so terrible is their racism.

But most people aren’t that extreme. We’ve just absorbed a whole lot of racism and sexism from the world we’ve lived our lives in, and that influences us. We’re a little bit racist, and that makes us a little bit bad – we have room for improvement. But we’re still, mostly, good people. The two-valued logic creates an apparent conflict where none really exists.

Where do these sexist/racist attitudes come from? Picture a scientist. What do you see in your minds eye? It’s almost certainly a white guy. It is for me. Why is that?

  1. In school, from the time that I got into a grade where we had a dedicated science teacher, every science teacher that I had was a white guy. I can still name ’em: Mr. Fidele, Mr. Schwartz, Mr. Remoli, Mr. Laurie, Dr. Braun, Mr. Hicken, etc.
  2. On into college, in my undergrad days, where I took a ton of physics and chemistry (I started out as an EE major), every science professor that I had was a white guy.
  3. My brother and I used to watch a ton of trashy sci-fi movie some free movie apps from the internet. In those movies, every time there was a character who was a scientist, he was a white guy.
  4. My father was a physicist working in semiconductor manufacturing for satellites and military applications. From the time I was a little kid until they day he retired, he had exactly one coworker who wasn’t a white man. (And everyone on his team complained bitterly that the black guy wasn’t any good, that he only got and kept the job because he was black, and if they tried to fire him, he’d sue them. I really don’t believe that my dad was a terrible racist person; I think he was a wonderful guy, the person who is a role model for so much of my life. But looking back at this? He didn’t mean to be racist, but I think that he was.)

In short, in all of my exposure to science, from kindergarten to graduate school, scientists were white men. (For some reason, I encountered a lot of women in math and comp sci, but not in the traditional sciences.) So when I picture a scientist, it’s just natural that I picture a man. There’s a similar story for most of us who’ve grown up in the current American culture.

When you consider that, it’s both an explanation of why we’ve got such a deeply embedded sexist sense about who can be a scientist, and an explanation how, despite the fact that we’re not deliberately being sexist, our subconscious sexism has a real impact.

I’ve told this story a thousand times, but during the time I worked at IBM, I ran the intership program for my department one summer. We had a deparmental quota of how many interns each department could pay for. But we had a second program that paid for interns that were women or minority – so they didn’t count against the quota. The first choice intern candidate of everyone in the department was a guy. When we ran out of slots, the guy across the hall from me ranted and raved about how unfair it was. We were discriminating against male candidates! It was reverse sexism! On and on. But the budget was what the budget was. Two days later, he showed up with a resume for a young woman, all excited – he’d found a candidate who was a woman, and she was even better than the guy he’d originally wanted to hire. We hired her, and she was brilliant, and did a great job that summer.

The question that I asked my office-neighbor afterwards was: Why didn’t he find the woman the first time through the resumes? He went through the resumes of all of the candidates before picking the original guy. The woman that he eventually hired had a resume that was clearly better than the guy. Why’d he pass her resume to settle on the guy? He didn’t know.

That little story demonstrates two things. One, it demonstrates the kind of subconscious bias we have. We don’t have to be mustache-twirling black-hatted villains to be sexists or racists. We just have to be human. Two, it demonstrates the way that these low-level biases actually harm people. Without our secondary budget for women/minority hires, that brilliant young woman would never have gotten an internship at IBM; without that internship, she probably wouldn’t have gotten a permanent job at IBM after graduation.

Professor Kulkarni said something silly. He knew he was saying something he shouldn’t have, but he went ahead and did it anyway, because it was normal and funny and harmless.

It’s not harmless. It reinforces that constant flood of experience that says that all scientists are men. If we want to change the culture of science to get rid of the sexism, we have to start with changing the deep attitudes that we aren’t even really aware of, but that influence our thoughts and decisions. That means that when someone says we did something sexist or racist, we need to be called on it. And when we get called on it, we need to admit that we did something wrong, apologize, and try not to make the same mistake again.

We can’t let the black and white reasoning blind us. Good people can be sexists or racists. Good people can do bad things without meaning to. We can’t allow our belief in our essential goodness prevent us from recognizing it when we do wrong, and making the choices that will allow us to become better people.