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

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.

---

As a further example let us define a dependently typed function where the return type will depend on the value argument.

Using Scala 3 facilities, consider the following heterogeneous list which maintains the precise type of each of its elements (as opposed to deducing a common least upper bound)

val hlist: (Int, List[Int], String)  = 42 *: List(42) *: "foo" *: Tuple()

The objective is that indexing should not lose any compile-time type information, for example, after indexing the third element the compiler should know it is exactly a String

val i: Int = index(hlist)(0)           // type Int depends on value 0
val l: List[Int] = index(hlist)(1)     // type List[Int] depends on value 1 
val s: String = index(hlist)(2)        // type String depends on value 2

Here is the signature of dependently typed function index

type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type] 
                                  |                     |        
                                 value           return type depends on value

or in other words

for all heterogeneous lists of type L, and for all (value) indices idx of type Int, the return type is Elem[L, idx.type]

where again we note how the return type depends on the value idx.

Here is the full implementation for reference, which makes use of literal-based singleton types, Peano implementation of integers at type-level, match types, and dependent functions types, however the exact details on how this Scala-specific implementation works are not important for the purposes of this answer which is mearly trying to illustrate two key concepts regarding dependent types

1. a type can depend on a value
2. which allows a wider set of errors to be eliminated at compile-time

// Bring in scope Peano numbers which are integers lifted to type-level
import compiletime.ops.int._

// Match type which reduces to the exact type of an HList element at index IDX
type Elem[L <: Tuple, IDX <: Int] = L match {
  case head *: tail =>
    IDX match {
      case 0 => head
      case S[nextIdx] => Elem[tail, nextIdx]
    }
}

// type of dependently typed function index
type DTF = [L <: Tuple] => L => (idx: Int) => Elem[L, idx.type] 

// implementation of DTF index
val index: DTF = [L <: Tuple] => (hlist: L) => (idx: Int) => {
  hlist.productElement(idx).asInstanceOf[Elem[L, idx.type]]
}

Given dependent type DFT compiler is now able to catch at compile-time the following error

val a: String = (42 :: "foo" :: Nil)(0).asInstanceOf[String] // run-time error
val b: String = index(42 *: "foo" *: Tuple())(0)             // compile-time error

scastie

Answer 3

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

Answer 5

I will try to provide an answer that goes straight to the chase.

A dependent type is the label used to indicate that the output's type (i.e. the type of the co-domain) depends on the actual input value/argument passed to the (dependent) function. e.g. F:forall a:A, Y(A) means the input type of F is A and that depending on the specific value of a the output type will be Y(a). So the output type depends on the input argument.

For a normal function we usually write f: A -> B which means that function f, any input of type A (informally \forall a \in A or a:A) returns some element of type B (informally some a \in B or b:A). That is a "normal" function type. However, a dependent type indicates that the output type of the (dependent) function F depends on the argument. Similarly, the output type is indexed (i.e. "depends") by the value of the argument. E.g. the notation I like (that nobody else uses afaik) is F: a:A -> Y(a) or the common notation F: forall a:A, Y(a). These notations simply say F takes some element a in A (i.e. of type A) and returns some element y of type Y(a) (or if you like index sets more use Y_a). It just means that the output type of F changes depending on the input value a to F.

A common example is a function F: forall n:Nat, Vector n which explicitly specifies the size of the array returned/outputed. So if you call F(a) then the output is of type Vector n which means it can only return a vector of size n denoted F(a):Y(a). As you can guess, if you always somehow guarantee this return type is respected, you make it harder to make out of bound errors (which is good for security).

I actually really like the Wikipedia article section on product types and think it's very thorough. If some part of it doesn't make sense of that small section ask me here I'm happy to clarify in the comments section https://en.wikipedia.org/wiki/Dependent_type#Formal_definition. Hope to explain in more detail what the article says in the future -- especially the what a product type means and it's relation to Cartesian products.