# Variary Functions in Coq

Often when I switch between Racket, my home language, and Coq, a research interest, I am struck by a minor but meaningful difference: Racket allows functions that vary in how many arguments they take, and Coq does not. It's minor, but it means that, for example, I cannot use this idiom:

(map + '(1 2 3) '(4 5 6) '(7 8 9)) ⇝ '(12 15 18)

This works because in Racket, `+`

takes any number of arguments and adds them all, and `map`

takes any number of lists as arguments (it picks one element from each and passes them as the arguments to the function).

In Coq, where every function has to not only run but also type-check, this sort of thing is harder to pull off because, for convenience's sake, functions are assumed to take one argument and curry. In this blog post, I describe my solution to a small puzzle posed to me by Talia: bridge the gap by implementing a function that takes any number of arguments and puts them in a list.

## Defining the type

The first challenge is giving such a function a type. I want the function to have `T → list T`

when I pass it one input and `T → T → T → list T`

when I pass it three inputs. Clearly we need to know ahead of time how many arguments to expect. If we expect `n`

arguments, we can define the type like so:

Fixpoint narg (n : nat) (T : Set) (U : Set) : Set := match n with | 0 => U | S n' => T -> (narg n' T U) end.

Here I've abstracted `list T`

to `U`

. In the heavily typed world of Coq, this sort of generality can actually be *good*, because it disciplines you and makes the proof search work better—I'll show you later.

Before dissecting the definition, here's some examples of it running:

Eval simpl in (narg 3). → fun T U : Set => T -> T -> T -> U

Note that `narg 3 T U`

is a *type*.

That looks correct! Looking through the cases, `narg`

takes an argument `n`

that tells it how many `T`

arguments a function will take before producing a `U`

. If we expect no types, then a function that expects 0 arguments before returning a `U`

is just a constant of type `U`

.^{1}^{1} In Racket, a function of no arguments and a constant are different things, but I think that's because of effects. I'll ignore the difference here. If we expect `n' + 1`

arguments, then we expect one argument before expecting `n'`

more before returning a `U`

.

Coq likes this definition; it is a simple recursion on `n`

, even though we're doing wild and wooly stuff like writing a function that returns a type.

## This way doesn't work

My first attempt looked something like this:

Definition nlist (n : nat) (T : Set) : narg n T (list T) := match n with | 0 => nil | S n' => fun t => cons t (nlist n' T) end.

This is definitely thinking in the right direction: with 0 arguments, we want to return `nil`

, and with `n + 1`

arguments we want to return a function that takes one argument and then conses it on to the list. But it doesn't type check, because `nlist n' T`

is not a list! It's a function waiting for god knows how many more arguments! We need to give that function all its arguments, and only then cons on the list.

This brought me to attempt number two:

Definition nlist (n : nat) (T : Set) : narg n T (list T) := match n with | 0 => nil | S n' => fun t => compose (fun tail => cons t tail) (nlist n' T) end.

This is closer: since `nlist n' T`

returns a function, and we want that function to run first and do something to the result, we want to use `compose`

. So we say: first, run `nlist n' T`

, which slurps up `n'`

arguments. Then, take the list it produced, and add `t`

to the front.

This is still not correct though, because Coq doesn't think of `nlist n' T`

as a function that takes `n'`

arguments; it thinks of `nlist n' T`

as a function that takes one argument, and returns a function, which by the way you cannot cons things on to.

In other words, I need, not a normal compose, but variary composition function.

## Variary composition

Variary composition should take a function from `n`

`T`

arguments to some output type `U`

, then some function we can apply to `U`

to get `V`

, and return a function that takes `n`

`T`

arguments and produces the final output `V`

. In Coq, this is:

Definition ncompose {n : nat} {T U V : Set} (f : U -> V) (g : narg n T U) : narg n T V.

Note that I finished this `Definition`

with a period—that means I will do the proof in tactic mode. This is a weird, worst-practice feature of Coq that I absolutely love, because it means I can use the power of proof search to write my programs for me. The downside is that proof search usually doesn't care what proofs it finds, whereas I generally care what my functions compute. This is why I carefully specified `narg`

to take a generic output type, instead of `list T`

. By forcing the left hand side of the composition, `g`

, and the result of the composition to return values of different types, I have written down a type with a single inhabitant for any given `n`

, so whatever proof search finds, it will work correctly.

The proof is simple:

crush

Ok, that's a joke, but only sort-of, in that `crush`

definitely finds the function. The non-=crush= solution is:

induction n; simpl in *; auto.

The induction is clear: with `0`

inputs we just want to apply `f`

to the constant that `g`

must be, and otherwise we want to do some other stuff that's recursive. But it turns out that simplifying the inductive hypothesis here yields a function `narg n' T U → narg n' T V`

, where `n' + 1 = n`

, whereas we need to produce a function `(T → narg n' T U) → (T → narg n' T V)`

. So it's just a normal composition away.

Finally, note that I've defined `n`

, `T`

, `U`

, and `V`

as implicit arguments in `ncompose`

, since they appear in the other arguments. This means you can use `ncompose`

like normal `compose`

if the right hand side has an `narg`

-based type.^{2}^{2} If it has a type like `T → T → U`

, Coq won't immediately know that that's just a reduction of `narg 2 T U`

, so you'll need to add types or implicit arguments somewhere.

(Since this is a tactic definition, remember to end it with `Defined.`

, not with QED, because we want the function to be something Coq can compute through.)

## Final function

Now that we have variary composition `nlist`

can be modified from the last failed attempt into a successful function:

Fixpoint nlist (n : nat) (T : Set) : narg n T (list T) := match n with | 0 => nil | S n' => fun t => ncompose (fun x => cons t x) (nlist n' T) end.

This works!

And to show that it really does the right thing (instead of just returning `nil`

), we can look at `nlist`

for particular `n`

:

Eval simpl in (nlist 3). ⇝ fun (T : Set) (t H H0 : T) => (t :: H :: H0 :: nil)%list

The syntax is as charmingly ugly as Coq usually is, but the point is that `nlist 3`

takes 3 `T`

arguments and puts them in a list in order.

## Taking this further

If you want to write a variary function, the easiest way to do it is to build on `ncompose`

and `nlist`

. For example, variary addition can be decomposed into gathering the arguments into a list:

Definition add (n : nat) : narg n nat nat := ncompose sum (nlist n nat).

and then summing them:

Fixpoint sum (l : list nat) : nat := match l with | nil => 0 | cons x rest => x + sum rest end.

Unfortunately, `n`

here cannot be made implicit, preventing you from evaluating `add 1 2 3 4`

. Instead, `n`

is explicit, so you have to write:^{3}^{3} I used `compute`

instead of `simpl`

here because, I think, `add`

isn't notated to expand when its first argument is in WHN form. If you add that notation, using some arcane Vernacular that I don't want to look up, it would probably work with `simpl`

as well.

Eval compute in (add 4 1 2 3 4). ⇝ 10

The reason `n`

can't be made implicit is that then Coq would be staring at `(add ?n) 1`

and it would only know that that function term had type `nargs ?n nat nat`

. Since `nargs`

matches on its first argument, `?n`

, Coq can't expand `nargs`

, so it can't find out that it is a function type. Since it can't figure that out, it's not sure that `add 1 2 3`

type checks!

## Even further, a challenge problem

Once we have `nlist`

in Coq, we can prove things about it. The easiest thing to prove would be that `nlist`

takes `n`

arguments and returns a list of length `n`

. The main challenge is stating the theorem.

The first step, I think, is to get the list length idea into Prop:

Definition has_length_n (n : nat) (T : Set) (l : list T) : Prop := length l = n. Theorem nlist_length : forall n T, ncompose (has_length_n n T) (nlist n T).

However, this doesn't quite work, because the type of that theorem statement is `narg n T Prop`

, instead of `Prop`

. That makes sense: we don't want to say that `nlist`

has length `n`

for all `n`

and `T`

. We also want to quantify over several arguments!

I sort of thought that something like this should work:

Fixpoint nforall (n : nat) (T : Set) (P : narg n T Prop) : Prop := match n with | 0 => P | S n' => forall (t : T), nforall n' T (P t) end. Theorem nlist_length : forall n T, nforall n T (ncompose (has_length_n n T) (nlist n T)).

But I think I am missing some wacky motive nonsense on the definition of `nforall`

, nonsense that doesn't get easier, sadly, in tactic mode. So I think I am a bit stuck here. I'd appreciate help!

In particular, I pose **as a challenge**: Find a way to implement `nforall`

with the expected semantics, and then prove `nlist_length`

.

*Update*: James has posted a solution to the challenge. The key is to allow relations on the output of two `narg`

calls. (His solution also changes `Set`

to `Type`

above to allow `Prop`

as an inhabitant.)

*Update*: Valentin points out that Coq's Numbers.NaryFunctions library replicates much of the functionality described here.

^{1}

^{2}

`T → T → U`

, Coq won't immediately know that that's just a reduction of `narg 2 T U`

, so you'll need to add types or implicit arguments somewhere.^{3}

`compute`

instead of `simpl`

here because, I think, `add`

isn't notated to expand when its first argument is in WHN form. If you add that notation, using some arcane Vernacular that I don't want to look up, it would probably work with `simpl`

as well.