Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is dependent typing?

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!

like image 753
Nick Avatar asked Feb 18 '12 04:02

Nick


People also ask

What is the meaning of dependent type?

In computer science and logic, a dependent type is a type whose definition depends on a value. It is an overlapping feature of type theory and type systems. In intuitionistic type theory, dependent types are used to encode logic's quantifiers like "for all" and "there exists".

How do dependent types work?

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

What is dependent program?

Updated: 10/17/2017 by Computer Hope. Software-dependent is a computer or hardware device designed for a software application. For example, a special computer may be set up and designed to work best with a CAD program.

What is dependent type programming in Python?

What is dependent typing? It is a concept when you rely on values of some types, not just raw types. Consider this example: from typing import Union def return_int_or_str(flag: bool) -> Union[str, int]: if flag: return 'I am a string!' return 0.


2 Answers

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.

like image 68
Andreas Rossberg Avatar answered Sep 23 '22 17:09

Andreas Rossberg


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

like image 31
Mario Galic Avatar answered Sep 23 '22 17:09

Mario Galic