A tremendous amount. Everybody's favorite example is fixed-size Vectors. You'd write them like data Vect : (n : Nat) -> (a : Type) where [] : Vec

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-to-write-a-function-in-haskell-r-a-r-a/25655429#25655429 http://stackoverflow.com/questions/25654641/is-it-possible-t...