I wanted to point you to two almost similar efforts [0] [1] then I found your post [2]. You may be interested also in [3].

[0] https://github.com/moonad/Formality

[1] http://imar.ro/~mbuliga/chemlambda-v2.html

[2] https://www.reddit.com/r/haskell/comments/dih8xu/optimal_red...

[3] https://mbuliga.github.io/kali24.html

I'm glad you find interest in this work.

Thank you for the links, I did not know we could do computation with... chemistry! As I'm not familiar with that, I do not understand everything. Can you point me to a list of the interactions of your system?

Formality indeed looks promising. I still have a lot to learn about EAL in order to forge my opinion, but maybe it is the "sweet spot". For example, Formality does not need a GC, whereas Éole does, which is time consuming. On the other hand, Éole (if it works) is completely general. But then, not being "completely general" isn't necessary a problem, and Formality seems to do very well.

Please note that Éole is not proven yet, and I'm looking for counter examples that might settle the case. I will actually be happy if someone "break" the system!

Sure, look at [2]. I commented on your github repo too.

EDIT: Re: the chemistry, I do think that it might be a big subject, see https://arxiv.org/abs/1811.04960 , which somehow is not very surprising because of the Algorithmic Chemistry (aka ALCHEMY) of Fontana and Buss.

Did you demonstrate that your trick is sound and optimal? Optimal reduction is a tricky beast and you might need to use a very high order function to find a counterexample.

A tricky beast indeed! No, the formal proof is a work in progress, so I'm also looking for counter-examples. And since posting on hackernews, someone found some problems (thank you so much Ekdohibs). However, there is for sure an implementation issue so they do not count as counter-examples yet. I'll investigate and fix that asap, then we'll see...

Does it have monads?

Of course not, monads are so 20th century... The October 2019 way is to only work with stacks of TripleZippersInvertedStateTransformerLens, and I know you know it!

Joke aside, it is supposed (I have some interesting bugs at the moment) to be an evaluator for the pure lambda calculus. So, I guess you can encode monads in it, but that is not really the point, and I definitely did not make an example with monads. I'll try to do such an example later.