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?
Can Elementary Affine Logic be used as the core type system of a practical programming language?
type theory
Something very similar, but using light affine logic (LAL) instead of EAL, was attempted a few years ago by Baillot, Gaboardi and Mogbil (you may find the paper here).  I think their work may be easily generalized to EAL, which is a more liberal system.As for the features of such language, you have polymorphism natively (EAL is a restriction of second order linear logic). As far as I know, no-one has looked at dependent types, but I don't see why they shouldn't work.  In fact, untyped EAL works just as well as typed EAL, because its normalization properties do not depend on types.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!In any case, if you are interested in the relationship between optimal evaluation, EAL and light logics in general, I suggest you take a look at Coppola's papers from the early to mid-2000s. 