Dependent Types

In this essay, I will consider how to design a good dependently typed language, with reference to Epigram [3] and Idris [5].

Expressiveness

The first obstacle to “goodness” is expressiveness: how do you ensure that there is enough in your language?

In the design of dependently-typed languages, expressiveness is perhaps most visible in the issue of (non-)termination. Allowing types to depend on terms means that equality requires normalisation. For example, one might define a dependent hd function that gets the head of a vector

\[ \texttt{hd :: Vec A (n+1)} \rightarrow \texttt{A} \]

To pass it a vector of type Vec A 4, I need to show that the types Vec A 3+1 and Vec A 4 are equivalent.

Assume a definition of equality on types (respectively terms), call it \(=_\text{T}\), and a set of normal forms \(N_T\), also equipped with a notion of equality (\(\cong_\text{T}\)). A normalisation function \(\textsf{norm}_T: T \to N_T\) is a function satisfying \(T_1 =_T T_2 \iff \textsf{norm}(T_1) \cong_\text{T} \textsf{norm}(T_2)\). We want the normalisation function to be total. It thus decides the equality of types (terms) [4].

The biggest worry is recursion, since it can lead to non-termination of the normalisation function. A helpful technique is to classify recursive functions into structurally recursive functions that are guaranteed to terminate, and generally recursive functions that may or may not terminate [6]. Informally, the compiler deems functions structurally recursive if it can verify that the size of the inputs decreases on each call. For example, foldl for List.

let rec foldl f z = function
 | [] -> z
 | x::xs -> foldl f (f z x) xs

Importantly, the definition of structurally “smaller” depends on a notion of order. The strength of our conclusions depends on this definition. For example, the foetus termination checker identifies structurally recursive functions, determining an order by considering three eliminators [1]:

1. \(y = C(x) \implies x < y\)
2. \(x < y \implies \pi_1 \, x < y \land \pi_2 \, x < y\)
3. \(f < y \implies \forall x. f \, x < y\)

Note that the final eliminator requires that \(y\) upper bound the image of \(f\). This is a strong condition, that might falsely classify some terminating programs as generally recursive. In the quicksort code below, the image filter (<=) is not upper-bounded by x::xs, and hence this analysis would class quicksort as generally recursive.

let rec qsort = function
 | [] -> []
 | x::xs -> qsort (filter (<= x) xs)
           @ [x]
           @ qsort (filter (> x) xs)

Indeed, since determining if a program terminates on an input is undecidable in general [11], any such analysis will classify some terminating programs as “generally recursive”.

The problem of expressiveness becomes clear: it seems that our programming language will either have a non-terminating type-checker or be Turing incomplete. How do we deal with the problem of termination while retaining expressiveness? Altenkirch et al. [3] outline three possible strategies for handling non-termination, which they term the “totalitarian”, “free market”, and “mixed economy” systems. In a sentence: the totalitarian bans general recursion, the libertarian allows general recursion everywhere, and the “mixed-economy” allows general recursion, but selectively.

Epigram opts for the “mixed-economy” approach, which I argue is the most expressive, and reveals a more general design strategy:

Less is More

It is clear that being less totalitarian results in more expressiveness. Unintuitively, being less liberal also gives you more expressiveness. The terminology is misleading: “totalitarian” and “liberal” describe the laws that the system enforces, not the manner of enforcement. Liberal laws are enforced illiberally. Take the example of termination. A liberal approach “demands an ignorance of totality” [8]. This reduces expressiveness: we cannot say “this function is total”, since by law, all functions might be partial. The mixed-economy is the only approach that avoids “global commitment”, either to totality or an ignorance of it [7].

Less is More is only a partial strategy: it tells us to carefully select the laws of a programming language, but not how to do so. The strategy is completed by another principle, by Harper [7]:

Appeal to Computational Trinitarianism

Rules of a programming language are axiomatic laws, and thus should hold as universal truths. Laws that should hold only some of the time, like “some functions are non-terminating”, are better implemented as principled extensions to the system, just as monads extend pure systems with effects. To determine which laws should be universal truths, Harper advises that we appeal to “Computational Trinitarianism”: the three-way connection between Type Theory, Proof Theory, and Category Theory. Laws should at least be well-behaved in all three theories.

This is precisely the principle that Altenkirch et al. appeal to when justifying their “mixed-economy”. They argue that to allow general recursion would be to permit, as a proof strategy, a “blatant [proof-theoretic] lie”:

\[ \forall P. (P \rightarrow P) \rightarrow P \]

In other words, it is not well-behaved as a proof method. However, in some cases, it may be selectively re-introduced [8]. The Curry-Howard Correspondence is thus operationalised as a yardstick in the design of programming languages.

Usability

A second obstacle is usability. The designs of Altenkirch et al. and Brady [5] consider the usability concerns that arise as the result of proof obligations. In dependently-typed languages, type checkers demand evidence in the form of proof.

These proof obligations impose an additional cost to the user. Take, for example, a dependently-typed accumulating reverse for Vector,

\[ \texttt{reverse\_acc: (xs : Vec A n)} \to {\texttt{(acc: Vec A m)} \to \texttt{Vec A (n+m)}} \]

The programmer is given the proof obligation

\[ \texttt{m'} + (1+ \texttt{n}) = 1 + (\texttt{m'} + \texttt{n}) \]

This requires commutativity of addition, which in turn relies on a lemma proving that \(0\) is a right unit for \(+\). For a programmer simply wanting to write a reversal function, this seems like a high cost. Altenkirch et al.’s [3] solution is incrementality. If the programmer decides the costs outweigh the benefits, they can impose less strict invariants, thereby reducing their proof goals:

\[ \begin{aligned} &\texttt{reverse\_acc\_weak: (xs : Vec A n)} \to {} \\ &\quad \texttt{(acc: Vec A m)} \to \exists \texttt{l}. \texttt{Vec A l} \end{aligned} \]

In my opinion, the strength of this argument depends on the goals of dependent types. Are we trying to allow programmers to write proofs? Or are we trying to encourage programmers to be more proof-oriented? This is an argument for the former, but not the latter. Altenkirch et al. acknowledge this, and set forth to employ “decision procedures” for simple “problem classes”.

In contrast, Brady equips Idris not only with an interactive tactics-engine, but allows for the use of “plugin decision procedures” as tactics, and additionally for custom tactics to be implemented. Perhaps he is envisioning a modular approach to programming with dependently typed languages, where engineers, theorem-provers, and tactics-builders specialise but collaborate. This modularity cannot be supported if the type-checker can only be given complete programs. The shed technology introduced by Altenkirch et al. solves precisely this problem. The programmer can use a shed as a to-do, and the type-checker can reason “around” sheds, thus working with partially written programs (with, for example, missing proofs).

In the spirit of readability, Brady proposes shunting proofs to the end of the file. A more structured approach might be to divide a module \(M\) into “\(M\).program” and “\(M\).proof” sub-modules, just as tests are not written in the same module as the code they test.

Reducing the costs of dependent types is one way to encourage their use. The other is to deliver benefits to programmers. Much has been said about the guarantees offered by dependently typed languages [4, 10]. I will instead focus on a more immediate benefit: interactivity via views [9]. Introduced by McBride and McKinna [9], and adopted by Brady, views illustrate that dependent types and pattern matching exhibit a synergy that makes their combination better than the sum of their parts.

The key idea is that pattern matching may be thought of as a decision tree, with two types of nodes. By nodes perform case analysis and expose inductive hypotheses. With nodes match on intermediate results. Dependent types enrich both of these.

By nodes are enriched since information carried by dependent types trims the pattern space. For example, if we define a function that takes in a Vec A (n+1), we do not need to consider the empty list as a pattern.

With nodes are enriched since pattern matching on an intermediate result refines our “view” of both values and types in the pattern (example by Brady):

data Parity : Nat -> Type where
 Even : Parity (n + n)
 Odd  : Parity (S(n + n))

parity : (n:Nat) -> Parity n

natToBin : Nat -> List Bool
natToBin Z = Nil
natToBin k with (parity k)
   natToBin (j + j)     | Even = False :: natToBin j
   natToBin (S (j + j)) | Odd  = True  :: natToBin j

Pattern-matching on the with node parity k == Even allows us to refine our pattern match from natToBin k to natToBin (j+j).

These views enhance usability in two key ways. First, they result in greater interactivity: the compiler can automatically generate the relevant by nodes, or update the view in response to a with node. This turns programming into a dialogue between programmer and compiler [3].

Second, views allow for more flexible pattern matching. We are used to pattern matching lists by considering a Nil and Cons case

  | [] -> ...
  | x::xs -> ...

But it is equally valid, and sometimes more convenient, to consider a Nil and Snoc case:

  | [] -> ...
  | xs@[x] -> ...

McBride and McKinna show how, by framing the Nil/Cons pattern as an induction scheme, views allow the user to define custom induction schemes (Nil/Snoc) [9].

Efficiency

A final obstacle is efficiency. In real-time systems, programs cannot just be correct: they must also be fast. Dependently-typed languages can provide guarantees about programs, but appear to be incompatible with low-level techniques like pointer arithmetic.

Brady illustrates one method for reconciling the two:

1. Write key functions, like reading and writing bits, in a low-level language (C),
2. Expose these functions via a foreign-function interface to a dependently typed language (Idris),
3. Compose them together in Idris

Hence, one gets the compile-time guarantees of Idris, and the run-time efficiency of C.

This approach is not without its faults. Any properties about the C functions (rather than their composition) have to be asserted rather than proven, since they are “external” to Idris [5]. Further, Brady does not measure its performance.

Without measurements, questions abound. I raise two other concerns. First, what if the most efficient version of the program is not structurally recursive? Second, while many types can be erased before run-time, can the compiler always detect these? Or, would the efficiency-minded user have to give explicit “run-time irrelevance” annotations, as in Agda [2]?

Conclusions

In conclusion, it is clear how to design an expressive dependently-typed language: via a minimalist approach. It is less clear how to build a usable language, but key inroads have been made. It is absolutely not clear, at least to me, how efficient our language can be.

References

1. [1] A. Abel. foetus – Termination Checker for Simple Functional Programs. arXiv:2407.06924. 2024. arxiv.org/abs/2407.06924
2. [2] Run-time Irrelevance — Agda 2.6.1 documentation. agda.readthedocs.io/en/v2.6.1/language/runtime-irrelevance.html
3. [3] T. Altenkirch, C. McBride, and J. McKinna. Why Dependent Types Matter. Unpublished manuscript. 2005.
4. [4] C. Angiuli and D. Gratzer. Principles of Dependent Type Theory. 2024.
5. [5] E. C. Brady. Idris — systems programming meets full dependent types. In Proceedings of the 5th ACM Workshop on Programming Languages Meets Program Verification, pages 43–54. 2011. doi.org/10.1145/1929529.1929536
6. [6] M. Felleisen, R. B. Findler, M. Flatt, and S. Krishnamurthi. How to Design Programs: An Introduction to Programming and Computing. The MIT Press. 2018.
7. [7] R. Harper. Introduction to Dependent Types Lectures, Oregon Programming Languages Summer School. 2015.
8. [8] C. McBride. Epigram: Practical Programming with Dependent Types. In Advanced Functional Programming, pages 130–170. 2005.
9. [9] C. McBride and J. McKinna. The view from the left. Journal of Functional Programming, 14(1), pages 69–111. 2004. doi.org/10.1017/S0956796803004829
10. [10] N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. SIGPLAN Not., 46(9), pages 266–278. 2011. doi.org/10.1145/2034574.2034811
11. [11] A. M. Turing. On Computable Numbers, with an Application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, s2-42(1), pages 230–265. 1937. doi.org/10.1112/plms/s2-42.1.230