You’ve seen equations before. For example here’s a few.
a = b
Ax^2 + Bx + C = y
x = {-b ± \sqrt {b^2 - 4ac} \over { 2a } }
Lets not discuss what these equations mean as they’re just examples of equations, besides they mean nothing without a type anyway. We’ll get back to that.
Now look at the = in these expressions. It divides them to two. It means that two sides of the equation have the same value.
What does “having a same value” mean? You know, it’s something we define in this formalism by deciding which properties we are interested about.
We can take something similar to Leibniz definition of equality and state that two terms x = y are equal, if all contexts that are available for them are equal. We could represent it like this:
{x = y \over P\ x = P\ y}congruence\ P
The horizontal line in the line means that we can turn the proposition given above the line, into the proposition given below the line.
You may have heard you’re comparing apples to oranges? Meaning you’re comparing things that cannot be compared. Well guess, there are ways they can be equal.
🍎🍎🍎=🍊🍊🍊
It depends on which type we pick on the equality because it determines how you’re interpreting this expression. That is, which type you are using.
For example lets say you’d observe this in terms of eating a fruit. We could write a rule such as:
{🍎🍎🍎 \over 🍎🍎} eat
Now we can see whether they’re equal.
🍎🍎🍎=🍊🍊🍊 \over eat \ 🍎🍎🍎=eat \ 🍊🍊🍊=🍎🍎
Is this right? Well it’d of course make a lot of sense if..
🍎=🍊
But that’s just a context that we just made up, and interpreted through that type apples and oranges are equal.
If you leave it to Leibniz equality, then the logic you use for equational reasoning would be extensional.
In practice we need to go a little bit deeper inside objects to tell whether they are equal. We need to define equality intensionally.
If you use intensional equality, then “terms have the same value”, means that they’re same if their internal definitions are same. Whether they’re “constructed” the same way.
We could define how the terms are constructed. For example with our fruits we could describe them with:
{\over ε}zero \quad {x \over x🍎}succ \quad 🍎=🍊
This gives us a form of equality that we can determine from the value. We get the following rules:
{\over zero = zero} \quad {x = y \over succ x = succ y}
These above are derivable with Leibniz equality and also produce it. However the intensional equality also gives a way to decide that two values aren’t equal.
{zero = succ x \over 0}zeroNotSucc
The 0 in this inference rule means for a type with no constructors. This means it’d be a contradiction if we happened to find out that 2 apples are 3 apples or similar.
We also say that terms are equal if they’re convertible to each other. \backsim in this text means that terms are convertible to each other.
\over {(x \backsim y) = (x = y)}
This rule connects the equality to computational medium. It means that the computation carried to any term will preserve the value of the term. To see why this is so, lets prove the following equation:
🍎+🍎🍎=🍎🍎🍎
Here’s the proof:
\def\arraystretch{1.1} \begin{array}{c} \\ \hline 🍎🍎🍎=🍎🍎🍎 ^{\{reflection\}} \\ \hline 🍎🍎🍎+ε=🍎🍎🍎 ^{\{reduction\}} \\ \hline 🍎🍎+🍎=🍎🍎🍎 ^{\{reduction\}} \\ \hline 🍎+🍎🍎=🍎🍎🍎 ^{\{reduction\}} \end{array} _{\blacksquare}
This is a valid proof if we have convertibility rules such as:
\def\arraystrech{1.1} \begin{array}{ccc} x+🍎y & \backsim & x🍎+y \\ x+ε & \backsim & x \end{array}
To do some equational reasoning, we need to extend the rules that we have for reasoning.
We already used this rule once, it is called reflection, or “refl” for short. This can be obtained from congruence.
{ \over x = x } refl
The equation can be manipulated in several ways such that the value stays same. One thing that we can do is exchange the terms over. This rule is called “commutativity”, or “exch”.
{ x = y \over y = x } exch
Equation composes, composition means that we can glue them together from terms to conclude something.
{ x = y,\, y = z \over x = z } composition
Our composition of equalities is associative.
{ f . (g . h) = (f . g) . h } = f.g.h
Types describe what properties a term has. This usually includes:
Type formation rules are rules for how a type is formed. These are similar to the construction rules for terms except that they describe how the type itself is constructed.
Terms get their interpretation of what type they are. Types are just like terms and they have a type as well.
Type of a type is an universe. Universe describes all types that you know how to construct.
Type of an universe is a higher universe and they go higher (or lower?), you get a yet higher (or lower?) universe whenever you need it.
Type theory is an academic study of type systems. Type theory was invented to avoid paradoxes that arise, for example, when you allow self-referential equations.
Types are judgemental in sense that they determine how you’re supposed to interpret a term, that is which rules that term obeys. Otherwise don’t assume anything about a term alone.
If the type is not provided with a term, you infer it from the context. If it’s vague which type it should be, you are required to denote the type with a typing judgment. Typing judgment separates a term from a type with a : -symbol.
term : type
The judgement means that we interpret this term with this type.
If a type has not been given and it’s not obvious from the context, then we assume that the term is a type itself. This is assumed because we’d end up with things such as:
zero:nat:type:type_1:type_2...
It’s better to stop the type lore before a type is mentioned.
For example, the constructors for natural number type would be described like this, possibly even if it was obvious from the context:
{\over zero : nat}zero \quad {x : nat \over succ \ x : nat}succ
We also have to denote type of values in expressions. It is used by giving the type of the value inside brackets after the equation:
x = y \{a\}
Equations themselves are types. I hope to make that obvious although I already gave you inference rules for equations.
By this basis, equality sign could be reinterpreted as something else in different context, but usually we keep the meaning same. This is done for a practical/technical reason, mainly, we have to map the concrete syntax to some abstract syntax and this is still usually done before we know the type of the term.
Eventually we’ll bring the knowledge of type theory and apply it to programming. Haskell programming language uses double-colon symbol (::) instead of : to denote a typing judgment.
term :: typeSome features in Haskell are detrimental for benefiting from type theory in full, notably:
We still mostly stick to Haskell in this book, because at the time of writing it is the best well-known functional programming language and it is very unlikely that it will be discarded any time soon.
Computers can be used to find proofs whenever inference rules are clear. In fact, any kind of computation can be interpreted as a proof-search.
You’ve already seen a similar instance of this phenomena in this chapter, but lets make it explicit with an example.
\def\arraystretch{1.1} \begin{array}{ccc} & 3 * (5 + 2) + 490 \\ ≻ & 3 * 7 + 490 \\ ≻ & 7 + 2 * 7 + 490 \\ ≻ & 7 + 14 + 490 \\ ≻ & 7 + 10 + 4 + 490 \\ ≻ & 10 + 10 + 1 + 490 \\ ≻ & 20 + 1 + 490 \\ ≻ & 20 + 491 \\ ≻ & 511 & \blacksquare \end{array}
When rules are used rather than defined, it ends with a black box that stands for Q.E.D. This makes it explicit when we are defining rules and when they are inferred from existing rules we’ve defined.
The ≻ stands for a computation step that has been founded to some set of convertibility rules. Computation flows downwards mainly to satisfy conventions commonly used to represent computation.
When we have a formal system where a computation eventually arrives to a solution, that is, doesn’t get stuck and eventually halts. It means that the language forms a formal logic where terms or programs can be treated as proofs for propositions that are in turn described with types.
In a well-designed computer system just having a term that is valid in respect to some type can be significant even if that term would be never used in a computation. These kind of terms confirm that computation has some property that we’ve described in a type to verify that the program is correct in respect to what we know.
1. Propositions in this book will eventually become more dense. They still retain similar content as presented here though.
Here’s denser representation of one of the exercises. Locate it from the text.
x = y \,\{a\}, P : a → b \over P \, x = P \, y \,\{b\}
We’ll get to what the arrow means in the next chapter.
2. If 0 stands for a type that you have no ways of constructing it, what does 1 stand for as a type? How about 2?
3. When numbers have multiple interpretations, how do you know how to interpret a number?
(more exercises needed)