<p>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.</p>

<p>Suppose we are given the following types:
<span class="math-container">\begin{align*}
&amp; \vdash A \ \mathsf{type} \\
x : A &amp; \vdash B(x) \ \mathsf{type} \\
x : A, y : B(x) &amp; \vdash C(x,y) \ \mathsf{type}
\end{align*}</span>
We would like the type of "binary" dependent functions whose domain is something like <span class="math-container">$x : A, y : B(x)$</span> and the codomain is <span class="math-container">$C(x, y)$</span>.</p>

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

<p>Without any pattern matching the type of dependent functions from <span class="math-container">$x : A, y : B(x)$</span> to <span class="math-container">$C(x, y)$</span> can be written as
<span class="math-container">$$\Pi (p : \{x : A, y : B(x)\}) \,.\, C(p.x, p.y),$$</span>
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
<span class="math-container">$$\Pi (\{x = x_0, y = y_0\}) \,.\, C(x_0, y_0).$$</span>
or, if we dare use the same symbol for a field label and the bound variable (OCaml allows this, for instance),
<span class="math-container">$$\Pi (\{x, y\}) \,.\, C(x, y),$$</span>
For such pattern matching to make sense we need to know ahead of time that the fields <span class="math-container">$x$</span> and <span class="math-container">$y$</span> have types <span class="math-container">$A$</span> and <span class="math-container">$B(x)$</span>, 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
<span class="math-container">$$\Pi (\{x : A , y : B(x)\}) \,.\, C(x, y)$$</span>
to indicate the missing type information.</p>

<p>Of course, the same sort of ideas apply to <span class="math-container">$\lambda$</span>-abstraction. Given
<span class="math-container">$$x : A, y : B(x) \vdash e(x,y) : C(x,y)$$</span>
the term
<span class="math-container">$$\lambda \{x : A, y : B(x)\} \,.\, e(x,y)$$</span>
will receive the above product type.</p>

<p>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 <em>concrete</em> examples of what you are looking for.</p>

CC BY-SA 4.0
2019-03-21T08:23:13.680Z
sorry. when asking the original question, it doesn't occur to me that the codomain of a Pi type can be defined by pattern matching, so I came up a convolved idea of adding a new primitive definitions of multi-arity functions. As now I realize that one can use pattern matching on record type, my question doesn't have much content now as it is based on a previous neglection.
molikto
CC BY-SA 4.0
2019-03-21T08:25:53.970Z
So your solution is exactly what I look for. it has the good property that funExt need not to be applied iteratively, also it is natural to define pattern matching as a operation on positive data types. So I wonder why this is not more widely used.
molikto
CC BY-SA 4.0
2019-03-21T07:24:07.823Z
2019-03-21T07:24:07.823Z
Andrej Bauer
<p>(cross posted from Reddit <a href="https://www.reddit.com/r/dependent_types/comments/b1ts8b/firstorder_multi_arity_functions_in_dependent_type/" rel="nofollow noreferrer">https://www.reddit.com/r/dependent_types/comments/b1ts8b/firstorder_multi_arity_functions_in_dependent_type/</a>?</p>

<p>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.</p>

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

<p>It turns out Sigma type has also some general properties like this: <a href="https://github.com/agda/cubical/blob/master/Cubical/Foundations/HLevels.agda#L66" rel="nofollow noreferrer">https://github.com/agda/cubical/blob/master/Cubical/Foundations/HLevels.agda#L66</a> . 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.</p>

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

<p>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.</p>

<p>Any related reference?</p>

CC BY-SA 4.0
2019-03-16T17:02:59.550Z
I do not understand what you're asking. Can you explain more previsely what you mean by  "primitive multi-arity function types"?
Andrej Bauer
CC BY-SA 4.0
2019-03-18T16:53:31.350Z
This sounds like it might be a question about currying in a dependent setting.  If  you can give a specific example it would be helpful.
user833970
CC BY-SA 4.0
2019-03-19T22:34:10.967Z
Don't functions _always_ have one and only one argument? :-)
xrq
CC BY-SA 4.0
2019-03-20T04:32:11.713Z
@user833970 let's say that a pi type's introduction rule is if A is a context extension of multiple variables and b is a value under the context extension, then Pi(A, b) is a valid pi type. something under these lines. so in this type theory there is four basic judgement: valid context, valid (multi-variable) context extension of a context, and valid type under a context, valid term of a context.
molikto
CC BY-SA 4.0
2019-03-20T14:18:32.970Z
And what would be wrong with replacing context extensions with dependent record types to achieve what you're asking for? The fact that then we're "encoding" things with record types? If so, what's the difference between a context extension and a dependent record type?
Andrej Bauer
CC BY-SA 4.0
2019-03-21T00:38:51.003Z
@AndrejBauer I thought before that in this way the codomain of pi will have a lot of projections which is kinda ugly to me. the problem is I've been thinking of record type as a negative type, but a record admitting a pattern matching should really be a positive type (which record can be seen as one) then this way it is more natural to think multiple arity functions defined by pattern matching as a one-arity function with record as domain, because pattern matching is really something defined for a positive type. (I still need to read more, but this is the idea I got
molikto
<dependent-type>
First-order multi arity functions in dependent type?
molikto
# First-order multi arity functions in dependent type?

(Asked by: username_0 on 2019-03-16)

(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?

**Tags:** dependent-type

> **Comments:**
> **username_1**: I do not understand what you're asking. Can you explain more previsely what you mean by  "primitive multi-arity function types"?  
> **username_2**: This sounds like it might be a question about currying in a dependent setting.  If  you can give a specific example it would be helpful.  
> **username_3**: Don't functions _always_ have one and only one argument? :-)  
> **username_0**: @username_2 let's say that a pi type's introduction rule is if A is a context extension of multiple variables and b is a value under the context extension, then Pi(A, b) is a valid pi type. something under these lines. so in this type theory there is four basic judgement: valid context, valid (multi-variable) context extension of a context, and valid type under a context, valid term of a context.  
> **username_1**: And what would be wrong with replacing context extensions with dependent record types to achieve what you're asking for? The fact that then we're "encoding" things with record types? If so, what's the difference between a context extension and a dependent record type?  
> **username_0**: @AndrejBauer I thought before that in this way the codomain of pi will have a lot of projections which is kinda ugly to me. the problem is I've been thinking of record type as a negative type, but a record admitting a pattern matching should really be a positive type (which record can be seen as one) then this way it is more natural to think multiple arity functions defined by pattern matching as a one-arity function with record as domain, because pattern matching is really something defined for a positive type. (I still need to read more, but this is the idea I got  

---

## 1 answers

### Answer by username_1 on 2019-03-21. Score: 1 | Accepted answer

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.

> **Comments:**
> **username_0**: sorry. when asking the original question, it doesn't occur to me that the codomain of a Pi type can be defined by pattern matching, so I came up a convolved idea of adding a new primitive definitions of multi-arity functions. As now I realize that one can use pattern matching on record type, my question doesn't have much content now as it is based on a previous neglection.  
> **username_0**: So your solution is exactly what I look for. it has the good property that funExt need not to be applied iteratively, also it is natural to define pattern matching as a operation on positive data types. So I wonder why this is not more widely used.  

---

