<p>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 <a href="http://perso.ens-lyon.fr/patrick.baillot/Publications/MESPAPIERS/BGM_ESOP2010.pdf" rel="noreferrer">here</a>).  I think their work may be easily generalized to EAL, which is a more liberal system.</p>

<p>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.</p>

<p>One consequence is that in EAL you may use arbitrary fixpoint of types (see for instance <a href="http://perso.ens-lyon.fr/patrick.baillot/Publications/MESPAPIERS/ELL_Ptime_Long_final.pdf" rel="noreferrer">this other paper</a> 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 <em>total</em>, 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).</p>

<p>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}$ <em>without</em> using iteration.  Then, you may iterate $\mathsf{dbl}$ to define the exponential function $\mathsf{exp}$ which, however, <em>cannot</em> 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!</p>

<p>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 <a href="http://dblp.uni-trier.de/pers/hd/c/Coppola:Paolo" rel="noreferrer">Coppola's papers</a> from the early to mid-2000s. </p>

CC BY-SA 3.0
2016-10-15T14:39:38.950Z
2016-10-19T09:25:33.850Z
2016-10-19T09:25:33.850Z
Damiano Mazza
<p>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. </p>

<p>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?</p>

CC BY-SA 3.0
2016-10-15T14:47:34.740Z
"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.
Damiano Mazza
CC BY-SA 3.0
2016-10-17T19:48:28.913Z
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
MaiaVictor
CC BY-SA 3.0
2016-10-18T08:43:17.720Z
Yes, that's correct.
Damiano Mazza
CC BY-SA 4.0
2019-09-21T12:46:58.773Z
"Anyway, no-one forbids you to try and see what you can get!" -- 3 years later: yes, nobody forbid me, so I did it! https://docs.formality-lang.org. Thanks for all your help :)
MaiaVictor
<type-theory>
Can Elementary Affine Logic be used as the core type system of a practical programming language?
MaiaVictor
# Can Elementary Affine Logic be used as the core type system of a practical programming language?

(Asked by: username_0 on 2016-10-13)

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?

**Tags:** type-theory

> **Comments:**
> **username_1**: "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.  
> **username_0**: 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  
> **username_1**: Yes, that's correct.  
> **username_0**: "Anyway, no-one forbids you to try and see what you can get!" -- 3 years later: yes, nobody forbid me, so I did it! https://docs.formality-lang.org. Thanks for all your help :)  

---

## 1 answers

### Answer by username_1 on 2016-10-15. Score: 11 | Accepted answer

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](http://perso.ens-lyon.fr/patrick.baillot/Publications/MESPAPIERS/BGM_ESOP2010.pdf)). 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](http://perso.ens-lyon.fr/patrick.baillot/Publications/MESPAPIERS/ELL_Ptime_Long_final.pdf) 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](http://dblp.uni-trier.de/pers/hd/c/Coppola:Paolo) from the early to mid-2000s.


---

