How to abstract over function arity in Lean and Coq?

Question

Given types $A, B$ I would like to express the type of all functions $f$ for which there exists an $n \in ℕ$ such that $f$ has type $A^n \to B$. And possibly in such a way, that for $a_1, \dots, a_n : A$ the expression $f a_1 \dots a_n$ is well-formed and of type $B$.

Is this possible to express using implicit coercions or so? Such a construction would help in formalising universal algebra. I know of this approach by Andrej Bauer, which makes the theory relatively easy to use, but the implementations are cluncky.

Edit: To clarify. I'd like to use such a construction to formalise universal algebra and apply the constructions and theorems of this theory to some concrete varieties (like boolean algebras, lattices, groups).

Usually in type theory, the operations of such algebras (e.g. groups) have types like $A \to A \to A$, when they are considered on their own. To have a good interaction of the formalisation of universal algebra with these definitions, it would be necessary that the operations are defined in a similar way. Otherwise one has to transfer between (fin 2 -> A) -> A and A -> A -> A.

Answer 1

I would like to focus on the following part of the question:

I'd like to use such a construction to formalise universal algebra and apply the constructions and theorems of this theory to some concrete varieties (like boolean algebras, lattices, groups).

Let us forget about formalization for a moment and recall how universal algebra is done mathematically. We shall use an unusually high level of precision to expose a piece of invisible mathematics that is making formalization difficult.

Given a number $n \in \mathbb{N}$, let $[n] = \{k \in \mathbb{N} \mid k < n\}$ be the set of numbers smaller than it.

A signature $\Sigma = (n, a)$ is a number $n \in \mathbb{N}$ with a map $a : [n] \to \mathbb{N}$. Intuitively $\Sigma$ describes an algebraic structure with $n$ operations, where the $i$-th operation has arity $a(i)$.

Remark: One would traditionally write $\Sigma$ as an $n$-tuple $(a(0), \ldots, a(n-1))$ of numbers, but we want to avoid ellipsis $\ldots$ and keep the level of precision high.

Let us continue. A $\Sigma$-structure $(S, f)$ is a set $S$ with a map $f : \prod_{i \in [n]} S^{[a(i)]} \to S$. Thus for each $i \in [n]$ we have a map $f_i : S^{[a(i)]} \to S$. This is a perfectly good general definition that works well when we want to prove theorems about all structures for an arbitrary signature $\Sigma$.

However, taking the definition literally and applying it directly to specific examples results in a great deal of clumsiness. Here's an example.

Example 1: Consider the signature $\Sigma = (3, \lambda i. i)$. Let $G = ([7], f)$ be the $\Sigma$-structure with $f : \prod_{i \in [3]} [7]^{[i]} \to [7]$ defined by \begin{align*} f_0(u) &= 0, \\ f_1(u) &= 7 - u(0), \\ f_2(u) &= (u(0) + u(1)) \mathbin{\mathrm{mod}} 7. \end{align*}

If you squint and think a bit, you will recognize that $G$ is a convoluted way of defining a cyclic group of order 7. Normal people define it as follows.

Example 2: Define $\mathbb{Z}_7 = ([7], e, i, m)$ where $e = 0$, $i : [7] \to [7]$ is defined by $i(k) = 7 - k$ and $m : [7] \times [7] \to [7]$ is defined by $m(k,m) = (k + m) \mathbin{\mathrm{mod}} 7$.

Examples 1 and 2 both define "essentially the same" structure. More precisely, there is an isomorphism $$\textstyle \left(\prod_{i \in [3]} [7]^{[i]} \to [7]\right) \cong [7] \times [7]^{[7]} \times [7]^{[7] \times [7]} $$ which can be used to translate between $G$ and $\mathbb{Z}_7$. However, you will not be able to find a book on universal algebra which does so explicitly. The formal difference between $G$ and $\mathbb{Z}_7$ is considered inessential, and identification of $G$ and $\mathbb{Z}_7$ convenient and harmless.

We may put back on our formalization hats. All of the ingredients above can be formalized in a straightforward way, except the identification of $G$ and $\mathbb{Z}_7$. The damn machine demands mathematical precision. So we are in an unfortunate situation that we know how to formalize both a general theory universal algebra and concrete examples of algebraic structures, but the two parts do not fit together easily.

I have no solution to offer, I just wanted to explain that this was a problem in formalization of invisible mathematics. If anyone knows a good solution, I would be interested to hear it.

Answer 2

You do not need coercions, instead you can define exactly the type you want: this is the magic of dependency. Here in Coq:

Require Import NArith.

Fixpoint nargs (A B : Type) (n : nat) :=
  match n with
    | 0 => B
    | S n' => A -> nargs A B n'
  end.

(* The type is exactly the one you expect *)
Eval cbn in nargs nat bool 3.
(* You can directly apply f, without any coercions *)
Check (fun f : nargs nat bool 3 => f 0 1 2).
(* You do not need the integer to be fully concrete, only to have enough successors *)
Check (fun (n : nat) (f : nargs nat bool (3+n)) => f 0 1 2).

Note that here you need to give the integer n explicitly. However, if you wish to, you can package things up:

Definition nargs' (A B : Type) := { n : nat & nargs A B n}.

But to use such an nargs' you will still need to unbundle it and look at the integer. This is only natural, though: $ f a_1 \dots a_n $ only makes sense if $f$ accepts at least $n$ arguments, and the type system needs to be enforcing this. You can even turn this idea into a function:

Definition enough {A B : Type} {m n : nat} (f : nargs A B n) (l : m <= n) : nargs A B (m + (n - m)) :=
  match (Minus.le_plus_minus m n l) with
    | eq_refl => f
  end.

(* enough lets you use an equality to expose enough constructor to enable application *)
Check (fun (n : nat) (f : nargs nat bool n) (l : 3 <= n) => (enough f l) 0 1 2).
```