How could one define a language based on the Calculus of Constructions, but with fixed points and EAL-style duplication restrictions?

Question

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.

Answer 1

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.