Why Dependent Types matter

tl;dr: With respect to expressive power in logic, Dependent Types matter because they allow us to express universal and existential quantification.

Most programming languages (Python, JavaScript) have the power to express propositional logic. For example, you can express AND, NOT, OR in Python, JavaScript or any other mainstream programming language. See my previous post Hierarchy of logical systems for more details on various logical systems.

However, if we are interested in mathematical proofs (and software correctness built upon those), then we need to work with higher order logic where we have the notion of universal (forall) and existential (exists) quantificators.

So, what are Dependent Types? Wikipedia formally defines them as:

Loosely speaking, dependent types are similar to the type of an indexed family of sets. More formally, given a type A:U in a universe of types U, one may have a family of types B:A->U, which assigns to each term a:A a type B(a):U. We say that the type B(a) varies with a.

This definition allows us to map (transform) terms to types, thus bringing closer the notion of values and types.

Let’s have a look at an Idris example of dependent types:

f : Nat -> Type
f Z = Bool
f x = String

As a result:

Idris> f 0
Bool : Type
Idris> f 1
String : Type
Idris> f 2
String : Type

Python example of “dependent types”:

def f(x):
	if x == 0:
		return bool
	else:
		return str

As a result:

>>> f(0)
<type 'bool'>
>>> f(1)
<type 'str'>
>>> f(2)
<type 'str'>

So we seem to be able to encode those in Python as well. But, there is no compile-step in Python to let us know that the types flow correctly.

So we can’t really take advantage of having the programming language do all the necessary logical checks for us in order to form a notion of mathematical proof.

Where Idris really shines is in the following example:

f : {a : Nat} -> GT a 0 -> String
f {a} proof_that_a_gt_zero = "It is type safe that " ++ (show a) ++ " is greater than zero!"

produce_necessary_proof : (a : Nat) -> LTE 1 (S a)
produce_necessary_proof a = (LTESucc {left=Z} {right=a}) (LTEZero {right=a})

safe : Nat -> String
safe Z     = "Whoops!"
safe (S x) = f (produce_necessary_proof x)

Let’s try to understand this example by breaking it up.

1. LTESucc and LTEZero is a constructor for the data type LTE. A few examples for LTEZero:

LTEZero : LTE 0 0
Idris> LTEZero {right = 1}
LTEZero : LTE 0 1
Idris> LTEZero {right = 2}
LTEZero : LTE 0 2

LTESucc allows us to say that if we have a proof of LTE a b then we can construct a proof of LTE (a + 1) (b + 1):

Idris> :t LTESucc
LTESucc : LTE left right -> LTE (S left) (S right)

GT a 0 is just a friendly wrapper around LTE 1 a.

2. Let’s try to explain what f, produce_necessary_proof and safe do.
So f is a function that takes any natural number greater than zero, and a proof that it is greater than zero, and outputs a string for it.

It’s like saying, mathematically, that forall x in N, x > 0 -> “It is type safe that {x} is greater than zero!”. We can see how close these relationships are represented.

So to produce the proof that a natural number is greater than zero (LTE 1 x), we implement produce_necessary_proof. Examples:

Idris> produce_necessary_proof 0
LTESucc LTEZero : LTE 1 1
Idris> produce_necessary_proof 1
LTESucc LTEZero : LTE 1 2
Idris> produce_necessary_proof 2
LTESucc LTEZero : LTE 1 3

safe then just combines f with produce_necessary_proof.

3. Compile-time checks that f only accepts a natural number greater than zero. While this is a purely mathematical example, we can also do industry examples…

Now, given all of the above, we can’t really do that in Python (or most mainstream languages) and have the compiler do all the checks for us and produce proofs for them 🙂