A tremendous amount.

Everybody's favorite example is fixed-size Vectors. You'd write them like

    data Vect : (n : Nat) -> (a : Type) where
      []    : Vect 0 a
      _::_  : a -> Vect n a -> Vect (n+1) a

and then we could statically ensure things like being incapable of taking the head of an empty Vect

    head : Vect (succ n) a -> a   -- even if n = 0, succ n = 1

Or, more cleverly, ensuring that two Vect append to their summed length

    (++) : Vect n a -> Vect m a -> Vect (n+m) a
    

But the real fun begins with things like "unsequencing"

    seq   : Vect n (a -> b) -> (a -> Vect n b)
    unseq : (a -> Vect n b) -> Vect n (a -> b)

Try to write that with plain lists [0] and you'll find that you are missing certain information about the inputs which make it impossible to do such that seq and unseq are mutual inverses.

You can define "zippy" `Applicative` instances for Vect which are not necessarily infinite (unlike List's ZipList instance). Also notice that the following definition of (<star>) is complete despite missing some "obvious" pattern matches... they can never arise and the types ensure it.

    instance Applicative (Vect n) where
      pure a = {- elided, but notice that this is tricky -}
      [] <*> [] = []
      (f :: fs) <*> (x :: xs) = f x :: (fs <*> xs)

We can also write a Traversable instance

    instance Traversable (Vect n) where
      traverse inj [] = pure []
      traverse (a :: as) = (::) <$> inj a <*> traverse as

and then we can get an "obvious" matrix transposition function

    type Matrix n m a = Vect n (Vect m a)

    transpose : Matrix n m a -> Matrix m n a
    transpose = traverse id

All of the functions above depend crucially upon the compile time invariant of having a fixed size list. They therefore work for any type-homogenous tuple, for instance, but we'd have to define the functions for each tuple independently. Using `Vect` we can classify the entire family of fixed-sized type-homogenous vectors all at once and dispatch functionality across the whole family.

As a final, much more sophisticated trick, we can look into why that seq/unseq bit worked. Essentially, what we have is that Vect n a is isomorphic with the function

    Vect n a ~ (Fin n -> a)

In other words, it's a function from the finite set of size `n` to values `a`. If we assume some isos and `flip`

    up : Vect n a -> Fin n -> a
    dn : (Fin n -> a) -> Vect n a

    flip : (a -> b -> c) -> (b -> a -> c)

then we can write seq/unseq trivially

    seq   : Vect n (a -> b) -> (a -> Vect n b)
    seq v a = dn (flip (up v) a)

    unseq : (a -> Vect n b) -> Vect n (a -> b)
    unseq f = dn (flip (up . f))

In a dependently typed language you can not only create types with these kinds of properties, express the isomorphism above, work generally over these kinds of structures, but you can even generalize the notion of "container" types, types which are functions from a particular shape to their values, in a way that is far more expressive than Haskell would allow.

---

And to be honest, all of the above are sort of silly examples. Far more sophisticated type invariants are routinely encoded in DT languages. It's hard to even begin talking about what's going on there.

[0] http://stackoverflow.com/questions/25654641/is-it-possible-t...

I really like your examples with the vector whose size is controlled by the type. However, is that useful in practice? I suppose that your vector would be read from a file or a database (especially if you do data analysis), in which case you can't know in advance - at compile time - what size the vectors will have.

I suppose it can still work if you want to do things with the covariance/correlation matrix: you may not know the number of rows before hand, but you know the number of columns, or know that two data sets will have the same number of columns.

The code you write doesn't necessarily fix an n, it just says that n cannot change in unprincipled ways throughout a computation. When you read in a vector from a database it will originally be unsized, but you can write code that shows the size is computed and left fixed and then from then on treat it as a sized vector.

It's hard to say exactly how useful this is in practice. More honestly, this is a rather trivial example mostly used to demonstrate DT.

One use of it is in implementing de Bruijn indexed lambda calculus interpreters---if you let the environment be a sized vector then you can use `n` to ensure there aren't bad variables in scope and to take note of closed expressions.

The n can come from the database, a file, or even user input from a text box. That's the point of dependent types: types can depend on run-time values.

Well, the n must "come from" the actual data. You could not construct a vector of any other size n. It'll just be typed so as to be realized at runtime and then maintained. The functions by-and-large do not ensure that the vector is sized for a particular n, but instead that they respect whatever n ends up being true.

Looking at Maybe/Option, it's clear that you can write a total function head' :: [a] -> Maybe a. This is good because it allows to represent the function's "failure" to return a head element with an unambiguous, non-magic sentinel value.

But really, in many cases you don't want to return "Maybe a" just because you did some operation that involved (somewhere in its middle) taking the head of a list. In some languages you would use "fromJust" or other fundamentally unsafe (in that they can lead the program to terminate abruptly if misused, and in that the compiler cannot help you use them properly) methods to present the interface you want. But ideally, you would have a head function that the compiler would only allow to be called on lists that can be proven non-empty, and which wouldn't need to wrap its return value in Maybe.

In a "typical" typesystem, encoding useful information (like how many times you can call tail on a list) into types can be very difficult. For this particular application, you could try to keep track of how many elements are in a list by constructing lists with a generic function that wraps the type it's given in a Cons<T> wrapper, but this approach can run into issues relatively quickly, depending on the language you're using. That said, in some typesystems which aren't fully dependently-typed, you can manage tricks like this, and they can solve this use-case in those contexts.

What full dependent types give you is the ability to have types depend arbitrarily on terms (values), such that lists whose types "know their length" are very simple to write, and much more complex guarantees about what your values get up to become possible to implement as types. The downside to this is that running the typechecking algorithm essentially requires arbitrary computation to be performed by the compiler; this can't always be guaranteed to terminate, and may take a few minutes even when it does.

I posted something at top level.