What is dependent typing?

Question

Can someone explain dependent typing to me? I have little experience in Haskell, Cayenne, Epigram, or other functional languages, so the simpler of terms you can use, the more I will appreciate it!

Answer 1

Consider this: in all decent programming languages you can write functions, e.g.

def f(arg) = result

Here, f takes a value arg and computes a value result. It is a function from values to values.

Now, some languages allow you to define polymorphic (aka generic) values:

def empty<T> = new List<T>()

Here, empty takes a type T and computes a value. It is a function from types to values.

Usually, you can also have generic type definitions:

type Matrix<T> = List<List<T>>

This definition takes a type and it returns a type. It can be viewed as a function from types to types.

So much for what ordinary languages offer. A language is called dependently typed if it also offers the 4th possibility, namely defining functions from values to types. Or in other words, parameterizing a type definition over a value:

type BoundedInt(n) = {i:Int | i<=n}

Some mainstream languages have some fake form of this that is not to be confused. E.g. in C++, templates can take values as parameters, but they have to be compile-time constants when applied. Not so in a truly dependently-typed language. For example, I could use the type above like this:

def min(i : Int, j : Int) : BoundedInt(j) =
  if i < j then i else j

Here, the function's result type depends on the actual argument value j, thus the terminology.

Answer 2

If you happen to know C++ it's easy to provide a motivating example:

Let's say we have some container type and two instances thereof

typedef std::map<int,int> IIMap;
IIMap foo;
IIMap bar;

and consider this code fragment (you may assume foo is non-empty):

IIMap::iterator i = foo.begin();
bar.erase(i);

This is obvious garbage (and probably corrupts the data structures), but it'll type-check just fine since "iterator into foo" and "iterator into bar" are the same type, IIMap::iterator, even though they are wholly incompatible semantically.

The issue is that an iterator type shouldn't depend just on the container type but in fact on the container object, i.e. it ought to be a "non-static member type":

foo.iterator i = foo.begin();
bar.erase(i);  // ERROR: bar.iterator argument expected

Such a feature, the ability to express a type (foo.iterator) which depends on a term (foo), is exactly what dependent typing means.

The reason you don't often see this feature is because it opens up a big can of worms: you suddenly end up in situations where, to check at compile-time whether two types are the same, you end up having to prove two expressions are equivalent (will always yield the same value at runtime). As a result, if you compare wikipedia's list of dependently typed languages with its list of theorem provers you may notice a suspicious similarity. ;-)

Answer 3

Dependent types enable larger set of logic errors to be eliminated at compile time. To illustrate this consider the following specification on function f:

Function f must take only even integers as input.

Without dependent types you might do something like this:

def f(n: Integer) := {
  if  n mod 2 != 0 then 
    throw RuntimeException
  else
    // do something with n
}

Here the compiler cannot detect if n is indeed even, that is, from the compiler's perspective the following expression is ok:

f(1)    // compiles OK despite being a logic error!

This program would run and then throw exception at runtime, that is, your program has a logic error.

Now, dependent types enable you to be much more expressive and would enable you to write something like this:

def f(n: {n: Integer | n mod 2 == 0}) := {
  // do something with n
}

Here n is of dependent type {n: Integer | n mod 2 == 0}. It might help to read this out loud as

n is a member of a set of integers such that each integer is divisible by 2.

In this case the compiler would detect at compile time a logic error where you have passed an odd number to f and would prevent the program to be executed in the first place:

f(1)    // compiler error

---

Here is an illustrative example using Scala path-dependent types of how we might attempt implementing function f satisfying such a requirement:

case class Integer(v: Int) {
  object IsEven { require(v % 2 == 0) }
  object IsOdd { require(v % 2 != 0) }
}

def f(n: Integer)(implicit proof: n.IsEven.type) =  { 
  // do something with n safe in the knowledge it is even
}

val `42` = Integer(42)
implicit val proof42IsEven = `42`.IsEven

val `1` = Integer(1)
implicit val proof1IsOdd = `1`.IsOdd

f(`42`) // OK
f(`1`)  // compile-time error

The key is to notice how value n appears in the type of value proof namely n.IsEven.type:

def f(n: Integer)(implicit proof: n.IsEven.type)
      ^                           ^
      |                           |
    value                       value

We say type n.IsEven.type depends on the value n hence the term dependent-types.

Answer 4

Quoting the book Types and Programming Languages (30.5):

Much of this book has been concerned with formalizing abstraction mechanisms of various sorts. In the simply typed lambda-calculus, we formalized the operation of taking a term and abstracting out a subterm, yielding a function that can later be instantiated by applying it to different terms. In SystemF, we considered the operation of taking a term and abstracting out a type, yielding a term that can be instantiated by applying it to various types. Inλω, we recapitulated the mechanisms of the simply typed lambda-calculus “one level up,” taking a type and abstracting out a subexpression to obtain a type operator that can later be instantiated by applying it to different types. A convenient way of thinking of all these forms of abstraction is in terms of families of expressions, indexed by other expressions. An ordinary lambda abstraction λx:T1.t2 is a family of terms [x -> s]t1 indexed by terms s. Similarly, a type abstraction λX::K1.t2 is a family of terms indexed by types, and a type operator is a family of types indexed by types.

• λx:T1.t2 family of terms indexed by terms

• λX::K1.t2 family of terms indexed by types

• λX::K1.T2 family of types indexed by types

Looking at this list, it is clear that there is one possibility that we have not considered yet: families of types indexed by terms. This form of abstraction has also been studied extensively, under the rubric of dependent types.