Can Elementary Affine Logic be used as the core type system of a practical programming language?

Elementary Affine Logic is a type system which captures the class of λ-terms that can be reduced in elementary time. Moreover, EAL-typeable terms can be reduced using the abstract fragment of Lamping's algorithm, which is particularly interesting to me because I'm exploring the corresponding interaction combinators.

My question is, how can one make a practical programming language using EAL as the underlying type system? I.e., what kind of extensions (fix-points, polymorphism, dependent types, datatypes, etc.) could be made to the core type system without affecting that characteristic, and would such a language be usable in practice, or would it be somehow too restrictive for reasons I'm not aware?

• "Elementary Affine Logic is a type system which captures the class of λ-terms that can be reduced in elementary time": this is imprecise. EAL captures a strict subset of $\lambda$-terms that represent elementary functions (w.r.t. the Church encoding). It is true that all elementary functions are covered: for each elementary function $f$, there is at least one EAL term computing $f$, but there are usually tons of other terms corresponding to elementary algorithms computing $f$ which are not in EAL. Commented Oct 15, 2016 at 14:47
• Woops, right. Also, as far as I understand, there are also terms that can be reduced with the abstract algorithm, but don't have an EAL type, right? So, while all EAL terms can be reduced without the oracle, there is still some mismatch between the abstract algorithm and EAL. @DamianoMazza Commented Oct 17, 2016 at 19:48
• Yes, that's correct. Commented Oct 18, 2016 at 8:43
• "Anyway, no-one forbids you to try and see what you can get!" -- 3 years later: yes, nobody forbid me, so I did it! docs.formality-lang.org. Thanks for all your help :) Commented Sep 21, 2019 at 12:46

One consequence is that in EAL you may use arbitrary fixpoint of types (see for instance this other paper by Baillot) and define data types in the natural recursive style (like $\mathtt{list\ A := nil\mathrel | A\ *\ list\ A}$), along with the less natural (from a programming perspective) system F definition. However, by the above remark on untyped normalization, a programming language based on EAL will always be total, which means that you won't have a fixpoint combinator and the use of recursive types is not as natural as you would expect. For instance, take Scott numerals: without recursive definitions (given by the fixpoint combinator) it is hard to express anything beyond constant-time operations with this representation of integers. Therefore, you will still need to use Church numerals for iteration (i.e., $\mathtt{for}$ loops), by using which you will incur in the fundamental stratification restriction of light logics (which gives them their complexity properties): you cannot iterate a function $\mathsf{Nat}\rightarrow\mathsf{Nat}$ which has itself been defined by iteration ($\mathsf{Nat}$ here is the type of Church integers).
An example: with some "Church integer hacking", it is possible to define in EAL $\mathsf{dbl}:\mathsf{Nat}\rightarrow\mathsf{Nat}$ such that $\mathsf{dbl}\ \underline{n} = \underline{2n}$ without using iteration. Then, you may iterate $\mathsf{dbl}$ to define the exponential function $\mathsf{exp}$ which, however, cannot itself be iterated. So whatever programming language based on EAL will need to have some kind of mechanism forbidding certain definitons by iteration; it s hard to imagine how such restriction would not result in a language which feels awkward to the programmer. Anyway, no-one forbids you to try and see what you can get!