First-order multi arity functions in dependent type?

Question

(cross posted from Reddit https://www.reddit.com/r/dependent_types/comments/b1ts8b/firstorder_multi_arity_functions_in_dependent_type/?

Take Agda for example, functions of multi arity is "encoded" as functions of one argument returning functions. In the same sense one can "encode" a record type as iterated Sigmas, but Agda has primitive first-order record type.

Then the problem is, in the encoded case, one can talk about functions of multiple arities generally, like function extensionality https://github.com/agda/cubical/blob/master/Cubical/Core/Prelude.agda#L105 . to apply function extensionality to functions of multiple arity, one just iteratively apply it multiple times.

It turns out Sigma type has also some general properties like this: https://github.com/agda/cubical/blob/master/Cubical/Foundations/HLevels.agda#L66 . So if record type is also encoded, then one can use this to a record type of multiple fields, just iterate it multiple times. But in case of Agda one cannot do this, because record type is primitive to Agda.

So is there a dependent type theory that has primitive multi-arity function types?

Also can we extends such a theory so we can talk generally of functions of multiple arity and records of multiple field? One goal is to write down a definition of "isContrRecord" in this new theory.

Any related reference?

Answer 1

I do not understand what you are asking for, as it seems that you are simply asking for record types. The comments are too terse for a normal discussion, so I will offer a solution here, and you tell us what is wrong with it. I will do it by way of an example.

Suppose we are given the following types: \begin{align*} & \vdash A \ \mathsf{type} \\ x : A & \vdash B(x) \ \mathsf{type} \\ x : A, y : B(x) & \vdash C(x,y) \ \mathsf{type} \end{align*} We would like the type of "binary" dependent functions whose domain is something like $x : A, y : B(x)$ and the codomain is $C(x, y)$.

Let us write $$ \{ \ell_1 : A_1, \ell_2 : A_2(\ell_1), \ldots, \ell_n : A_n(\ell_1, \ldots, \ell_{n-1}) \} $$ for a dependent record type with fields $\ell_i$. Observe that this looks a lot like a chunk of a context. Given a term $p$ of the above type, write $p.\ell_i$ for the $i$-th projection.

Without any pattern matching the type of dependent functions from $x : A, y : B(x)$ to $C(x, y)$ can be written as $$\Pi (p : \{x : A, y : B(x)\}) \,.\, C(p.x, p.y),$$ which is arguably not so nice. But since patterns for record types are irrefutable (they always match), we can also use pattern-matching to write $$\Pi (\{x = x_0, y = y_0\}) \,.\, C(x_0, y_0).$$ or, if we dare use the same symbol for a field label and the bound variable (OCaml allows this, for instance), $$\Pi (\{x, y\}) \,.\, C(x, y),$$ For such pattern matching to make sense we need to know ahead of time that the fields $x$ and $y$ have types $A$ and $B(x)$, respectively. In implementations of proof assistants this is typically not a problem as each record type has to be declared before it can be used. Otherwise, we can still write something like $$\Pi (\{x : A , y : B(x)\}) \,.\, C(x, y)$$ to indicate the missing type information.

Of course, the same sort of ideas apply to $\lambda$-abstraction. Given $$x : A, y : B(x) \vdash e(x,y) : C(x,y)$$ the term $$\lambda \{x : A, y : B(x)\} \,.\, e(x,y)$$ will receive the above product type.

In any case, it seems that we can have pattern matching on the records and get precisely what you are asking for. I kindly ask that, in case this is not what you are asking for, you modify your question and provide some concrete examples of what you are looking for.