Writing a variadic currying function using dependent types

Oftentimes in programming, there will be a function that can obviously be generalized to an arbitrary number of arguments, and it would be convenient to be able to handle each of the generalized versions of this function in some sort of uniform manner.

One common approach is to use template metaprogramming, which allows for source code creation at compile-time. In this post, we will demonstrate how one can leverage a sufficiently expressive dependently-typed type system to write such “variadic functions” at the term level, without using any metaprogramming. As an example, we will write a function that can curry a function of arbitrary arity (and whose tupled argument can be entirely heterogeneous). We wrote this currying function in Coq, although this approach should translate to most other dependently-typed languages out there. You can find the source code here.

We don’t claim that this approach is practically useful, but hopefully it can give some people a better idea of how powerful true dependent types can be.

Typing the function

Before we can even begin writing out the function, we need to be able to express its type. Using informal ellipsis-based notation, we would say that such a function should have the type

$\forall n \forall X_1 \ldots X_n Y. (X_1 \times \ldots \times X_n \rightarrow Y) \rightarrow X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y.$

We see then that we’ll need some way to handle an arbitrary number of universal quantifiers, as well as arbitrarily-sized versions of the product and exponential on types.

As a first step, let’s define the type of n-ary functions on types:

$\begin{align*} \mathsf{Ty} &: \mathsf{nat} \rightarrow \mathsf{Type}\\ \mathsf{Ty}_0 &:= \mathsf{Type}\\ \mathsf{Ty}_{n+1} &:= \mathsf{Type} \rightarrow \mathsf{Ty}_n \end{align*}$

Given such a type-level function, we can turn it into a type via the universal closure, which captures each type variable under a universal quantifier:

$\lambda X_1 \ldots \lambda X_n. \Phi[X_1,\ldots,X_n] \mapsto \forall X_1 \ldots \forall X_n. \Phi[X_1,\ldots, X_n]$

Once again, this can be defined recursively in a fairly straightforward fashion:

$\begin{align*} \mathsf{UC} &: \forall n. \mathsf{Ty}_n \rightarrow \mathsf{Type}\\ \mathsf{UC_0}(T) &:= T\\ \mathsf{UC_{n+1}}(F) &:= \forall X. \mathsf{UC_n}(FX) \end{align*}$

With that out of the way, we see that it suffices now to define the follow type-level function:

$\lambda X_1 \ldots \lambda X_n \lambda Y. (X_1 \times \ldots \times X_n \rightarrow Y) \rightarrow X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y : \mathsf{Ty}_{n+1}$

For the sake of brevity, we won’t go into exact detail on how to define this, but it’s worth mentioning some of the combinators on type-level functions that are required:

Given a type-level function, increase the arity by one by adding an unused argument at the end:

$\Phi \mapsto \lambda X_1\ldots\lambda X_n\lambda Y.\Phi X_1 \ldots X_n$

Given a unary type-level function and a type-level function, apply the unary function underneath all the lambda abstracted arguments:

$F, \Phi \mapsto \lambda X_1\ldots\lambda X_n. F(\Phi X_1 \ldots X_n)$

Given a binary type-level function and two type-level functions of matching arity, apply the binary function to both underneath all the lambda abstracted arguments:

$F, \Phi,\Psi \mapsto \lambda X_1\ldots\lambda X_n. F(\Phi X_1 \ldots X_n)(\Psi X_1\ldots X_n)$

Defining the function

With the type defined, we can finally move on to actually defining the function in question. First, notice that for each arity, the currying function is the unique function with type

$(X_1 \times \ldots \times X_n \rightarrow Y) \rightarrow X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y.$

Thus, we will reduce the question of defining each currying function to the question of inhabiting each such type.

To show that each of these types is inhabited, we proceed by induction on the arity, starting at one (it does make sense to start at zero, but then the types for tuples would have $\ldots \times \mathbf{1}$ ’s at the end, which is somewhat annoying).

For our base case then, we need something of type

$(X \rightarrow Y) \rightarrow X \rightarrow Y.$

Of course, we can use the identity function here.

For the inductive step, we assume we have something of type

$(X_1 \times \ldots \times X_n \rightarrow Y) \rightarrow X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y$

and we need to define something of type

$(X_0 \times X_1 \times \ldots \times X_n \rightarrow Y) \rightarrow X_0 \rightarrow X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y.$

To see how this can be done, let’s see those two types with common subterms highlighted:

$({\color{Blue} X_1 \times \ldots \times X_n} \rightarrow {\color{Green} Y}) \rightarrow {\color{Orange} X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y}$

$({\color{Red} X_0} \times {\color{Blue} X_1 \times \ldots \times X_n} \rightarrow {\color{Green} Y}) \rightarrow {\color{Red} X_0} \rightarrow {\color{Orange} X_1 \rightarrow \ldots \rightarrow X_n \rightarrow Y}$

After removing the details, we have these two types:

$({\color{Blue} P} \rightarrow {\color{Green} Q}) \rightarrow {\color{Orange} R}$

$({\color{Red} S} \times {\color{Blue} P} \rightarrow {\color{Green} Q}) \rightarrow {\color{Red} S} \rightarrow {\color{Orange} R}$

which means we need something of type

$(({\color{Blue} P} \rightarrow {\color{Green} Q}) \rightarrow {\color{Orange} R}) \rightarrow ({\color{Red} S} \times {\color{Blue} P} \rightarrow {\color{Green} Q}) \rightarrow {\color{Red} S} \rightarrow {\color{Orange} R}$

and this is a basic STLC exercise.

After a bit of maneuvering to ensure that type arguments are passed around in the correct manner, we can finally define our variadic currying function. Let’s see how it works:

Compute variadic_curry 10.

yields

= fun (X X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 : Type) (x : uncurried_type 10 X X0 X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (x0 : X) (x1 : X0) (x2 : X1) (x3 : X2) (x4 : X3) (x5 : X4) (x6 : X5) (x7 : X6) (x8 : X7) (x9 : X8) (x10 : X9) => x (x0, (x1, (x2, (x3, (x4, (x5, (x6, (x7, (x8, (x9, x10)))))))))) : curry_type 10

which is indeed what we wanted.

Written on March 3, 2019