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