Dependent type

Consider the $\begin{array}{l}\\ texthead\end{array}$ function which returns the first item of a list.

• Elaboration

  • Simple types can say "this is a list" but not "this is a list of length 5".

  • Dependent types extend Curry-Howard correspondence to predicate logic:

    • $\forall$ becomes $\mathrm{\Pi }$ (dependent function).

    • $\exists$ becomes $\mathrm{\Sigma }$ (dependent pair).

  • Types can mention values, so preconditions become part of the signature, enforced by the compiler.

• Example

  Consider the $\text{head}$ function which returns the first item of a list.

  $$\text{head}:\text{List}a\to a$$

  Based on the signature, this must either:

  • Crash on empty lists.

  • Return $\text{Maybe}a$.

  • Lie.

    -> With dependent types, the precondition is the caller's proof obligation-no runtime check, no partiality.

    -> A safe head function on vectors:

    $$\text{head}:\text{Vec}(n+1)a\to a$$

    -> The type guarantees length $\ge 1$.