Previously: Models of (Dependent) Type Theory.
There is a deep connection between mathematics and programming. Computer programs deal with such mathematical objects as numbers, vectors, monoids, functors, algebras, and many more. We can implement such structures in most programming languages. For instance, here’s the definition of natural numbers in Haskell:
data Nat where Z :: Nat -- zero S :: Nat -> Nat -- successor
There is a problem, though, with encoding the laws that they are supposed to obey. These laws are expressed using equalities. But not all equalities are created equal. Take, for instance, this definition of addition:
plus :: Nat -> Nat -> Nat plus Z n = n plus (S n) m = S (plus n m)
The first clause tells us that is equal to . This is called definitional equality, since it’s just part of the definition. However, if we reverse the order of the addends and try to prove , there is no obvious shortcut. We have to prove it the hard way! This second type of equality is called propositional.
In traditional mathematics equality is treated as a relation. Two things are either equal or not. In type theory, on the other hand, equality is a type. It’s a type of proofs of equality. When you postulate that two things are equal, you specify the type of proofs that you are willing to accept.
Equality is a dependent type, because it depends on the values that are being compared. For a pair of values of the type , the identity (or equality) type is denoted by :
(In this notation, assumptions are listed above the horizontal line.)
You’ll also see written as , or even , if the type is obvious from the context.
... continue reading