Wouldn't the calculus of constructions with linear types be a simple functional core that is consistent and expressive? I have recently asked if there is a simple functional core that is consistent and expressive. In another question, cody pointed out that this is an open problem to have a language that is:


Consistent/Normalizing
Can express all the type families from Coq (or even Agda)
Allows for a simple expression of recursion over these families
Simple or has a small number of core constructions (Π,Σ,μΠ,Σ,μ).


Now, suppose we take the elementary affine logic and extend it with dependent types and fix. It is easy to prove that language is consistent and normalizing as a consequence of EAL. It can, I believe, express all the type families from Coq, with lambda-encodings and since it has fix. A simple expression of recursive algorithms is possible with church-encodings for iteration and scott-encodings for matching. And it is obviously simple, as it only has ∀, ! and let. Moreover, such language would have the very comforting property that it can be reduced optimally using the abstract fragment of Lamping's algorithm.

All things considered, such language looks like a perfect candidate for the role of a small functional core that serves as an universal code-interchange format, as proposed by Gabriel. Is my suspicion correct, or is there any problem with this reasoning?
This is a tough question to answer, since simplicity is in the eye of the beholder.

Certainly $\lambda$-encodings have their drawbacks, there are reasons why Coq decided to move away from them, the most obvious one is the inability to introspect the subterms during recursion. The second is the general awkwardness in defining deeply or mutually recursive functions.

As you note, the "fix-encoding" avoids this but then it is hard to define non-constant functions (which is the point Damiano brings up)! You have to choose: introspection or recursion. Often we want both.

I'm also a bit skeptical of Gabriel's proposal: how does he compute exponentials on "native" ints without recursion?

In addition, the fact that EAL can only express elementary functions seems intuitively like it should restrict "natural" ways of writing recursions. In particular this shouldn't be well-defined:

Fixpoint acker m := match m with
| O =&gt; S
| S m =&gt; (fix acker' f n := match n with
    | O =&gt; f 1
    | S n =&gt; f (acker' f n)
    end)
   (acker m)
end.

since it defines a non-elementary function. So what feature of EAL is preventing this definition? If I understand correctly (and I'm not sure I do), the term f (acker' f n) cannot be well-typed, there must be some "stratum" which prevents the final application of f.

So certainly the natural way to write this function is forbidden. What other natural things are forbidden in this framework? It's hard to say without asking a specialist, but my guess is that there will be a fair number of things. Linear type systems can be powerful frameworks, but they aren't very convenient or natural for writing programs.

It's also an important fact (but maybe this is asking for a lot) that $0\neq 1$ is directly provable in Coq, thanks to large elimination. Is adding this feature easy in your proposal?

Finally, there's something I'm always worried about when I hear about type systems with linear logic: how hard is it to write a type checker? Certainly the checker has to figure out which pieces of the context go where when performing checking. Also the user or the front-end has to figure out where to put all the !s, if you want to have any non-linear components (and you usually do!).

To summarize, my answer to the question "is EAL with dependent types simple, consistent and expressive?" is probably not: it is probably consistent, but I'm not sure it's simple, and I don't think it is sufficiently expressive.

However, there is a "simple" way to refute this claim: write down the system definition, ideally prove it consistent, and write down some simple functions using it, probably up to, say, red-black trees or something. If the fully detailed syntax and typing rules is large, then the system is complex, if it is very tough to write down the functions, then it is insufficiently expressive. If it is neither of those, then you've answered a tough open problem in type theory!