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!

  • So what exactly didn't you understand about e.g. the wikipedia article? – Karl Knechtel Feb 19 '12 at 4:28
  • 84
    Well, the article opens with lambda cubes, which sound like some type of sheep meat to me. Then it goes on to discuss λΠ2 systems, and as I don't speak alien I skipped that section. Then I read about the calculus of inductive constructions, which incidentally seems to have little to do with calculus, heat transfer, or construction. After giving a language comparison table, the article ends, and I am left more confused than when I got to the page. – Nick Feb 19 '12 at 5:50
  • @Nick That’s a general problem with Wikipedia. I saw your comment a few years ago, and I’ve remembered it since. I’m bookmarking it now. – Daniel H Nov 11 '15 at 0:40
up vote 76 down vote accepted
+50

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.

  • Isn't the BoundedInt example actually a Refinement Type, though? That's 'pretty close' but not exactly the kind of 'dependent types' that, e.g., Idris mentions first in a tutorial about dep.typing. – Noein Jun 29 '15 at 22:32
  • 2
    @Noein, refinement types indeed are a simple form of dependent types. – Andreas Rossberg Jun 30 '15 at 18:00

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. ;-)

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.

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

Your Answer

 

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Not the answer you're looking for? Browse other questions tagged or ask your own question.