0
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ I do not understand what you're asking. Can you explain more previsely what you mean by "primitive multi-arity function types"? $\endgroup$ – Andrej Bauer Mar 16 at 17:02
  • 1
    $\begingroup$ 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. $\endgroup$ – user833970 Mar 18 at 16:53
  • 1
    $\begingroup$ Don't functions always have one and only one argument? :-) $\endgroup$ – xrq Mar 19 at 22:34
  • $\begingroup$ @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. $\endgroup$ – molikto Mar 20 at 4:32
  • $\begingroup$ 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? $\endgroup$ – Andrej Bauer Mar 20 at 14:18
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – molikto Mar 21 at 8:23
  • $\begingroup$ 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. $\endgroup$ – molikto Mar 21 at 8:25

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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