[ImprobableTruth]

If you're familiar with refinement types, what he's mentioning is using dependent types to achieve refinement types.

Let's take the typical example of "lists of size n". It's either a special inductive type vec A n, or a list l with a proof that length l > 0. The signatures of a head function (using Coq syntax, where this approach is most common) would be:

  head_safe1 {A n} : vec A (S n) -> A
  head_safe2 {A} : forall (l : list A), length l > 0 -> A.

In both cases you match on the list and prove the nil case to be impossible.

One benefit is that one can easily stack predicates. Need a list of length n that is also sorted? Just add an argument of type Sorted l.

Programs that are 'truly' dependently typed have their benefits, but they definitely can feel more rigid.