3
$\begingroup$

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 need a lot of boilerplate.

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.

$\endgroup$
8
  • 1
    $\begingroup$ In lean, A^n is usually written as fin n -> A; does this work for your purposes? $\endgroup$ Mar 14 at 9:46
  • $\begingroup$ You can then also maybe add a coercion from (fin n.succ -> A) -> B to A -> (fin n -> A) -> B, but I'm tempted to say that may be a bit annoying. $\endgroup$ Mar 14 at 9:47
  • 1
    $\begingroup$ The approach you link to serves a different purpose, namely to formalize the theory of $n$-ary operations, not to actually use them in a formalization. $\endgroup$ Mar 14 at 11:39
  • 2
    $\begingroup$ There's a key piece of prior work on this in Agda by Guillaume Allais, who discusses exactly what features are required from the type checker to make usage of such functions ergonomic. pureportal.strath.ac.uk/en/publications/… $\endgroup$
    – James Wood
    Mar 14 at 15:13
  • 1
    $\begingroup$ @8bc3457f: I elaborated my comment, but it took the form of an answer. $\endgroup$ Mar 14 at 22:03

2 Answers 2

2
$\begingroup$

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).

Such a definition is included in the Coq std. library: Numbers.NaryFunctions.nfun. 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).
$\endgroup$
2
  • $\begingroup$ Thanks. I'll try how this works out. $\endgroup$
    – 8bc3 457f
    Mar 14 at 14:13
  • $\begingroup$ I only found some time to work on this now. The paper linked in the comment of mudri (to the question) seems essential to me for this approach. I immediately need to state assumptions of Proper for such functions, which might be doable with the techniques of that paper. $\endgroup$
    – 8bc3 457f
    Mar 30 at 7:49
5
$\begingroup$

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.

$\endgroup$
6
  • $\begingroup$ When defining your notion of structure, you fixed a way to "decode" a signature into a type, namely $\prod_{i \in [n]} S^{[a(i)]} \to S$, and you then say you would rather have another type (isomorphic to the first) as decoding. But you can define that other type as the decoding instead (it will look like the nargs in my answer, defined by induction on the signature and then on each arity). $\endgroup$ Mar 16 at 10:58
  • $\begingroup$ Whether this is a good idea is not entirely clear to me: it might make the universal algebra more painful than necessary. But you can for sure show at the universal algebra level that the two decodings are always isomorphic, and so you can turn an instance of the second decoding into one of the first if you wish to apply universal algebra theorems that are easier to show on that side. $\endgroup$ Mar 16 at 10:58
  • 1
    $\begingroup$ I am pretty sure the other type will make proofs parametereized by general signatures more paniful. $\endgroup$ Mar 16 at 12:37
  • 2
    $\begingroup$ The claim that "you can turn an instance of the second decoding into one of the first if you wish" is repeated often and convincingly – but nobody every does this, and everybody just imagines that it can be done. This is the crux of my observation, namely that the claim is just a myth. $\endgroup$ Mar 16 at 12:38
  • $\begingroup$ I think that part of the problem is actually the next step, ie going from an iterated product of functions to a primitive notion like a record with multiple fields (one for each operations). Usually, language support for bundling things is at that level, and you do not benefit from it if you merely stay at the level of (iterated) products. $\endgroup$ Mar 16 at 18:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.