From logic and math to code. For dummies. Part III. Dependent types

In the previous parts (1, 2) we were talking about formal logic and its evolution. We also considered implication, universal quantification and existential quantification. Now it’s time to build a strong bridge between math notions and programming implementations.

But firstly, let’s talk about what actually type is. We use type to restrict data, which comes to our program. For example type Int is a set of numbers from −2,147,483,648 to 2,147,483,647. Allowing all possible values of this set is called Int type. So any of such values can be encoded with 32 bits and now it’s easy to work with it and be sure about memory safety. But usually our logic notions are much more complicated, so we need a really advanced theory to build basically any kind of restriction over the data.

From 1934 to 1969 independently Haskell Curry and William Howard have been observing the correspondence between formals systems and models of computation. Let’s look at the result of this generalization, which was called later as Curry-Howard Correspondence:

As we are already familiar with left side of the table, so let’s see what we have in the right column.

Product type

One of the most usable types ever. Corresponds to logical AND. Structs in C and Rust, classes in Java, objects in JavaScript, records in Haskell are product types. Basically most of the object orienting programming based on this type. In math notion the following type

type A = {a: number, b: string}

sounds as “The set of all (a, b) where a is a number and b is a string”

Sum type

Very well known type in various systems, also called as enum or union.

type A = number | string

Both product and sum types are most common classes of algebraic types. Which means basically any kind of composite type. So now we can deal not with primitive type only, but with their composition.

Dependent product type (П type)

Here the fun comes. Because we have to apply quantifications to types.

As you remember from logic part, quantification is a generalization over implication (there are some/all clouds, which cause raining)

If implication is a function in Curry-Howard correspondence, then we need somehow to influence arguments and the result of that function to apply a quantification. And now the type of our result depends on argument, which is not common for programming languages. Usually they do not depend on each other at all. Compiler just expects a type which we pointed out.

Function with argument x and type F(x) is called П type. x can be any value, we don’t restrict it, which means it is a universal quantification ∀

Now, let’s have a look what we have:

{
    x1: F(x1),
    x2: F(x2)
    ...
}

And what was a simple product type:

{
   a: T1,
   b: T2
}

Looks similar, right? But like the higher level of generalization.

Dependent sum type (Σ type)

For П type we saw that it’s related to universal quantification because we can apply any argument to our function. Our type consisted of set of pairs x: F(x). In opposite, Σ type corresponds to only one of such pairs (it’s also called dependent pair). It reflects the meaning of existential quantification: “there is at least one”. There is a certain value and function which type depends on this value. We can union multiple such types (that will be called disjoint union)

x: F(x) | y: F(y) | z: F(z)

Let’s compare with simple sum type:

number | string

Why do we need all of this?

Safety

As you can see, most of the programming languages don’t care about any kind of complicated types. But they have to pay for that with run time errors, when the actual value of variable goes out of the expected range, causing program crashing or unexpected behavior.

All the strong typed languages are aimed to make programs as safe as it possible before running. Support of algebraic types allows you to protect everything on the type level (Haskell, Rust, Scala) and dependent types allow to add value level restrictions in compile time, which makes programs even more safe (Idris, Coq). For example you can be sure about List length and don’t get into index is out of range problem.

One another advantage is that once you described your logic in types it’s likely will work after refactoring. If the program is compiled successfully, then the logic is still correct.

Proof assistants

Writing a program in Haskell or Idris sometimes looks like preparation of documents for a bureaucratic institution. It’s hard to collect and fill everything out correctly from the first attempt, but if it’s passed — you have a solid paper. Having dependent types we actually test our types against predicates and if the program is compiled, then it means that our proof is correct and doesn’t have any logical collisions.

Sounds promising right? Just describe your topic of arguing in Idris, Coq or Agda and it will decide who is right and who is wrong. Politicians should be scared.

But coming back to the first part, our brain has another nature and such laborious preparation is just usually not worth it. So commercial use of automated theorem proving is mostly concentrated in integrated circuit design and verification. We think by probabilities and 60% for us is already more than enough. So seems like we need … strong typed probabilistic programming language.

But that’s already another story.

Find me in Twitter