The difference between dependent type signatures and proofs

Question

With dependent types, you can either capture function properties in the type signature, like in concatenation with length-indexed lists

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

or you can not use dependent types in your signature, like concatenation with standard lists

(++) : List a -> List a -> List a

and write proofs about (++)

appendAddsLength : (xs, ys : List a) -> length (xs ++ ys) = length xs + length ys

lengthNil : length [] = 0

lengthCons : (x : a) -> (xs : List a) -> length (x :: xs) = length xs + 1

Is there any difference between these approaches beyond ergonomics?

Answer 1

The most obvious difference is that, with (++) on Vects, the length is statically known: you can operate on it at compile time. Moreover, you don't need to write any additional proofs in order to ensure that (++) has the expected behavior on Vects, whereas you need to do it for Lists.

That is, (++) on Vect is correct by construction. The compiler will always enforce the desired properties, whether you like it or not, and without the user taking any additional action.

---

It's important to note that length xs is not really interchangeable with the statically-known size in general. On these data types, length is a function which actually re-computes the length of a List or Vect by walking through it and incrementing a counter:

libs/prelude/Prelude/Types.idr:L403-L407

namespace List
  ||| Returns the length of the list.
  public export
  length : List a -> Nat
  length []        = Z
  length (x :: xs) = S (length xs)

libs/base/Data/Vect.idr:25-28

public export
length : (xs : Vect len elem) -> Nat
length [] = 0
length (_::xs) = 1 + length xs

Even with Vect, the length built into to the type by construction, but the result of applying the length function to a List or Vect is not fundamental at all. In fact, Data.Vect contains a proof that Data.Vect.length that applying length to a Vect n t always returns n:

libs/base/Data/Vect.idr:30-34

||| Show that the length function on vectors in fact calculates the length
export
lengthCorrect : (xs : Vect len elem) -> length xs = len
lengthCorrect []        = Refl
lengthCorrect (_ :: xs) = rewrite lengthCorrect xs in Refl

Using the above proof, we can assert statically, without actually executing length, that the result of length is propositionally equal to the statically-known length of the Vect. But this assurance is not available for List. And it's much more cumbersome to work with in general, likely requiring the use of with ... proof and rewrite a lot more than just using the correct-by-construction type.