Show HN: Eole, a Lévy-optimal lambda calculus evaluator written in Rust

Show HN: Eole, a Lévy-optimal lambda calculus evaluator written in Rust(github.com)

106 points by HerrmannM 6 years ago | 9 comments

xorand 6 years ago |

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

HerrmannM 6 years ago | |

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!

xorand 6 years ago | | |

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

danharaj 6 years ago |

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.

HerrmannM 6 years ago | |

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

voldacar 6 years ago |

Does it have monads?

HerrmannM 6 years ago | |

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!

HerrmannM 6 years ago | | |

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.