If you want a take-home tag line for DTLs, here you go:
A dependently-typed language is one where the type system is the same as the language itself.
This means that types are first-class objects. You can pass them as arguments. You can return them as return values.
In a function signature, you may give names for all your arguments. For example: index : (n : Nat) -> List Int -> Int.
The names are brought into scope inside the type. This means that arbitrary values may end up living "inside the types". A "better" version of the type above might be index : (n : Nat) -> Vect n Int -> Int. Here, we use Vect instead of List -- the difference is that a Vect n A is known to have exactly n elements of type A. (In constrast, a List A might have fewer or more than n elements).
Using this trick, we can do all sorts of cool things. As hinted above, index : (n : Nat) -> Vect n Int -> Int pulls out the n-th element of a list of integers. (Btw, Nat stands for natural number. These are the integers without the negative ones). The cool thing is that while something like myList[10] might cause a runtime error (or worse, a buffer overflow), using index, we can guarantee a compile time that such an error is impossible. (Additionally, a good compiler might be able to compile it down to code as fast as C -- no bounds checking, but also no chance of segfaults or exploits).
Of course, this additional type safety comes at a price. We must now keep track of the length of our lists everywhere we go. This isn't quite as hard as it might sound, but it does add some complexity. But DT languages like Idris are geared towards letting you decide how much safety you need for your application.
Another interesting feature of DTLs is that not all types are inhabited. In every other language you use, every type has a constructor. (Even for abstract types where you cannot call it yourself... someone constructs an object for you at some point and hands it to you). In DTLs, it is advantageous to have empty types: types which absolutely positively cannot be instantiated no matter what.
Why would we want such a useless thing? Because being unable to create an object of a given type makes it impossible to do something. And maybe that something is something you shouldn't be doing anyway. Here's an example:
Suppose I have defined a function Nonzero : Nat -> Type. It takes a natural number as an input and gives you back a type as output. (Remember types are first-class!) We define it in Idris like this:
Nonzero : Nat -> Type
Nonzero Z = _|_
Nonzero (S n) = ()We might think of Nonzero as a 'family' of types: we get a type for every natural number: Nonzero 0, Nonzero 1, Nonzero 2, ... etc. But we were clever in our definition. The notation _|_ means the empty type (it's pronounced "bottom"), and () is the trivial type (pronounced "unit" by Haskellers, although we might have called it "top"). This means that the type Nonzero 0 is impossible to create, but Nonzero 1, Nonzero 2, etc are all easy to create.
So now, we have a type which corresponds to a property about our program. If n is some natural number, maybe given by the user... maybe the length of a list... maybe the number of lines in a file.... If it's possible to create an object of type Nonzero n, then we can guarantee n is nonzero.
A practical example: saving the world from division by zero!
We (partially) define division as follows:
div : (n : Nat) -> (d : Nat) -> Nonzero d -> Nat
div n Z p = absurd p
div n (S n) () = ...The ... is the hard part where you actually do the division algorithm. But the point I want to focus on is that in the case that d = 0, we can completely avoid having to write code for what happens when we divide by zero.
Looking at the type, let's try calling div. If we want 4 / 2, we see: div 4 2 : Nonzero 2 -> Nat. But Nonzero 2 reduces down (because it's a function), and it reduces to (). We then get div 4 2 () : Nat is a natural number (and if we implemented the algorithm correctly, we get the number 2).
But what about 2 / 0? What then? Well, we see: div 2 0 has type Nonzero 0 -> Nat. But we said above that we can't produce an object of type Nonzero 0! It's impossible. And in turn, division by zero is also impossible. Win!
In the implementation, we see that in the case of d = Z we use a function absurd (Z means zero by the way, and S means "successor" or "+1"). The absurd function allows you to declare that we have proven that execution branch is unreachable, and that we need not concern ourselves with it.
Those are my two favorite examples of what DTLs are.
Some other major themes in DTLs I should mention:
Testing can be suplemented with theorem proving. Tests rarely have full coverage. A theorem is like a test, but allows you to show a property holds for all input values. Absolutely all of them.
(Well-typed) Metaprogramming is possible. Many languages have macro systems. But macros are, from the perspective of a strongly-typed programmer, very unsafe. (They suffer from the same sorts of problems as SQL injection and Cross-site Scripting in web development). Dependent types are powerful enough that you can embed arbitrary sub-languages into the type system as DSLs.
To give a little more concrete examples of when this would be useful. Dependent types have the power to subsume GHC's Generic Deriving, Dynamic and Typeable, and Generalized Newtype Deriving extensions. It allows you to do variable argument functions, as Brian McKenna showed earlier today on r/programming with printf. Edwin Brady has been working on a library that allows effectful programming with multiple effects without resorting to painful monad stacks.
So, that's my pitch. Let me know how I did.