Dependent types [closed]

Question

A while ago I come across the programming language Idris which "unique selling point" seem to be dependent types. Can someone explain what dependent types are and what kind of problem they are addressing?

Answer 1

Well, dependent types allows for expressing data type invariants that are checked during compile time. The canonical example for dependent types is the length-indexed lists, also known as vectors. The Idris definition of vectors is:

data Vec (A : Type) : Nat -> Type where
   Nil  : Vec A 0
   Cons : A -> Vec A n -> Vec A (S n)

where type Nat corresponds to natural numbers in Peano notation:

data Nat = Z | S Nat

Note that, Vec A type is what we call a type family: for each value n : Nat we have a type Vec A n, of vectors of length n.

Having length in its type allows for some list functions to be correct by construction. A simple example is a safe list head function:

head : Vec a (S n) -> a
head (x :: xs) = x

Since we demand that only non-empty vectors are passed to head function - note the index S n demands non-zero values - Idris compiler guarantees that head will never be applied to empty lists.

Other example, is concatenation of vectors that ensures that its results have length equal to the sum of its parameters length:

(++) : Vec a n -> Vec a m -> Vec a (n + m)
[] ++ ys = ys
(x :: xs) ++ ys = x :: (xs ++ ys)

Note that the concatenation-length property is guaranteed by concatenation function type. Other application is to prove that traditional map function on vector preserves its length:

map : (a -> b) -> Vec a n -> Vec b n 
map f [] = []
map f (x :: xs) = f x :: map f xs

Again, the vector-length preservation is ensured by map type annotation. These are very simple examples of how dependent types help to ensure correct by construction software.

More convincing examples of dependently typed programming (using Agda programming language) can be found in The Power of Pi. I haven't done this, but I believe that all examples of this paper can be ported to Idris without difficulties.