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