<p>Dependency is interesting because of equality, and equality is adjoint to contraction. As a result, substructural calculi (which in general omit contraction) do not have an obvious notion of equality.</p>

<p>In type-theoretic language, equality is characterized by the following inference rule[*] being valid in both directions (top-to-bottom and bottom-to-top):</p>

<p>$$
\begin{array}{l}
\Gamma, x:\tau, y:\tau \;|\; \Theta, x = y : \tau \vdash P \\
\hline
\Gamma, z:\tau \;|\; [z/x,z/y]\Theta : \tau \vdash [z/x,z/y]P \\
\end{array}
$$</p>

<p>This says that if you have two free variables $x$ and $y$, and an assumption they are equal, that lets you derive the same things are replacing them both by a variable $z$. Note that going from top to bottom is a <strong>contraction</strong> -- the number of uses of $z$ will be the sum of the uses of $x$ and $y$. </p>

<p>As a result, interpreting the meaning of equality in linear calculi is tricky. The obvious thing to do is to restrict your attention to types which are contractible, but it turns out there are multiple incomparable ways of doing so! </p>

<p>One idea, originating in the work on Linear LF by Cervesato and Pfenning, is to only permit dependency on exponential types. </p>

<p>I, with Nick Benton and Pierre Pradic, gave another calculus based on another version of this idea, which exploited Benton and Wadler's characterization of linear logic in terms of an adjunction between a cartesian closed category and a monoidal closed category. Basically, we just made the CCC part dependent, so that linear types could be dependent on intuitionistic types, but not vice-versa. (However, you could be dependent on <em>closed</em> linear terms, since they are duplicable.) </p>

<p>In his PhD thesis, Matthijs Vákár gave a denotational model of Linear LF. His semantics was based on Benton-Wadler adjoint models, so it should also interpret our calculus.</p>

<p>The other main idea is due to Conor McBride, with subsequent refinements by Bob Atkey. His idea is based on resource interpretations of linear logic, with the idea that if you forget the resource usage information on a linear term, you are left with a nonlinear term approximating it. Then, you can depend on that nonlinear term.   </p>

<p>[*] This inference rule is for the case of first-order logic. The dependent case is more complicated, but the underlying issues are the same.</p>

CC BY-SA 3.0
2017-11-16T15:50:46.410Z
Wait... how does this address this question? Are you saying that a language with dependent types based on EAL wouldn't be useful for proofs because you don't have a clear notion of equality, because expressing `Refl` requires duplication?
MaiaVictor
CC BY-SA 3.0
2017-11-16T17:42:04.450Z
@MaiaVictor: I mean that, and also something even stronger. If the same variable can occur multiple times within a type expression, interpreting what types mean without contraction being semantically valid is very hard.
Neel Krishnaswami
CC BY-SA 3.0
2017-11-16T18:40:24.287Z
that raises many more questions. For one, did you mean "same variable **can't** (not **can**)? For two, afaik, there are other notions of equality that not necessarily use duplications. And finally, what would you recommend me to read to catch up with all that work? Or, better: how could I find an advisor with that knowledge? But, of course, asking further questions in comments is demanding, so don't worry about replying this comment if you don't have enough time.
MaiaVictor
CC BY-SA 3.0
2017-11-16T23:37:46.860Z
(It would be very cool if you could reference the work you mention!)
MaiaVictor
CC BY-SA 3.0
2017-11-16T12:44:52.623Z
2017-11-16T12:44:52.623Z
Neel Krishnaswami
<p>Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, give us a simple core with dependent types that can be reduced on the oracle-free fragment of Lamping's abstract algorithm. </p>

<p>Now, it has been shown [1] that adding type-level fixed points to EAL do not affect its complexity bounds. Doing so would make the language more interesting, as one would be able to define induction and inductive types. Problem is, the Calculus of Constructions makes no distinctions between types and values. As such, adding Fix would imply its existence on the value level (except if we make an exception of the rule, which looks inelegant), which may cause non-termination. </p>

<p>As such, it is not obvious to me how to add Fix to the language of the first paragraph without inhabiting all types. Perhaps a restricted version of it, with fix variables only occurring on non-application positions (i.e., only as arguments) would suffice, but I'm not sure 1. if that's true, 2. if that'd be the right way. </p>

<p>[1] J.-Y. Girard. Light linear logic. Information and Computation,
143:175–204, 1998.</p>

<type-theory><lambda-calculus><linear-logic><calculus-of-constructions>
How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?
MaiaVictor
# How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?

(Asked by: username_0 on 2017-11-14)

Suppose that we take the Calculus of Constructions as a basis, but take away exponential functions (allowing only linear functions), and add the controlled duplication rules of EAL. That'd, I believe, give us a simple core with dependent types that can be reduced on the oracle-free fragment of Lamping's abstract algorithm.

Now, it has been shown [1] that adding type-level fixed points to EAL do not affect its complexity bounds. Doing so would make the language more interesting, as one would be able to define induction and inductive types. Problem is, the Calculus of Constructions makes no distinctions between types and values. As such, adding Fix would imply its existence on the value level (except if we make an exception of the rule, which looks inelegant), which may cause non-termination.

As such, it is not obvious to me how to add Fix to the language of the first paragraph without inhabiting all types. Perhaps a restricted version of it, with fix variables only occurring on non-application positions (i.e., only as arguments) would suffice, but I'm not sure 1. if that's true, 2. if that'd be the right way.

[1] J.-Y. Girard. Light linear logic. Information and Computation,
143:175–204, 1998.

**Tags:** type-theory, lambda-calculus, linear-logic, calculus-of-constructions

---

## 1 answers

### Answer by username_1 on 2017-11-16. Score: 2

Dependency is interesting because of equality, and equality is adjoint to contraction. As a result, substructural calculi (which in general omit contraction) do not have an obvious notion of equality.

In type-theoretic language, equality is characterized by the following inference rule[\*] being valid in both directions (top-to-bottom and bottom-to-top):

$$
\begin{array}{l}
\Gamma, x:\tau, y:\tau \;|\; \Theta, x = y : \tau \vdash P \\
\hline
\Gamma, z:\tau \;|\; [z/x,z/y]\Theta : \tau \vdash [z/x,z/y]P \\
\end{array}
$$

This says that if you have two free variables $x$ and $y$, and an assumption they are equal, that lets you derive the same things are replacing them both by a variable $z$. Note that going from top to bottom is a **contraction** -- the number of uses of $z$ will be the sum of the uses of $x$ and $y$.

As a result, interpreting the meaning of equality in linear calculi is tricky. The obvious thing to do is to restrict your attention to types which are contractible, but it turns out there are multiple incomparable ways of doing so!

One idea, originating in the work on Linear LF by Cervesato and Pfenning, is to only permit dependency on exponential types.

I, with Nick Benton and Pierre Pradic, gave another calculus based on another version of this idea, which exploited Benton and Wadler's characterization of linear logic in terms of an adjunction between a cartesian closed category and a monoidal closed category. Basically, we just made the CCC part dependent, so that linear types could be dependent on intuitionistic types, but not vice-versa. (However, you could be dependent on *closed* linear terms, since they are duplicable.)

In his PhD thesis, Matthijs Vákár gave a denotational model of Linear LF. His semantics was based on Benton-Wadler adjoint models, so it should also interpret our calculus.

The other main idea is due to Conor McBride, with subsequent refinements by Bob Atkey. His idea is based on resource interpretations of linear logic, with the idea that if you forget the resource usage information on a linear term, you are left with a nonlinear term approximating it. Then, you can depend on that nonlinear term.

[\*] This inference rule is for the case of first-order logic. The dependent case is more complicated, but the underlying issues are the same.

> **Comments:**
> **username_0**: Wait... how does this address this question? Are you saying that a language with dependent types based on EAL wouldn't be useful for proofs because you don't have a clear notion of equality, because expressing `Refl` requires duplication?  
> **username_1**: @MaiaVictor: I mean that, and also something even stronger. If the same variable can occur multiple times within a type expression, interpreting what types mean without contraction being semantically valid is very hard.  
> **username_0**: that raises many more questions. For one, did you mean "same variable **can't** (not **can**)? For two, afaik, there are other notions of equality that not necessarily use duplications. And finally, what would you recommend me to read to catch up with all that work? Or, better: how could I find an advisor with that knowledge? But, of course, asking further questions in comments is demanding, so don't worry about replying this comment if you don't have enough time.  
> **username_0**: (It would be very cool if you could reference the work you mention!)  

---

