10 ms·

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

106 points by HerrmannM 7y ago

xorand 7y 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 https://github.com/moonad/Formality [1] http://imar.ro/~mbuliga/chemlambda-v2.html http://imar.ro/~mbuliga/chemlambda-v2.html [2] https://www.reddit.com/r/haskell/comments/dih8xu/optimal_reduction_without_oracle_prototype/ https://www.reddit.com/r/haskell/comments/dih8xu/optimal_red... [3] https://mbuliga.github.io/kali24.html https://mbuliga.github.io/kali24.html
- HerrmannM 7y 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 7y ago
    Sure, look at [2]. I commented on your github repo too.
    - xorand 7y ago
      EDIT: Re: the chemistry, I do think that it might be a big subject, see https://arxiv.org/abs/1811.04960 https://arxiv.org/abs/1811.04960 , which somehow is not very surprising because of the Algorithmic Chemistry (aka ALCHEMY) of Fontana and Buss.
danharaj 7y 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 7y 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 7y ago
Does it have monads?
- HerrmannM 7y 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 7y 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.

106 points by HerrmannM 7y 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 https://github.com/moonad/Formality [1] http://imar.ro/~mbuliga/chemlambda-v2.html http://imar.ro/~mbuliga/chemlambda-v2.html [2] https://www.reddit.com/r/haskell/comments/dih8xu/optimal_reduction_without_oracle_prototype/ https://www.reddit.com/r/haskell/comments/dih8xu/optimal_red... [3] https://mbuliga.github.io/kali24.html https://mbuliga.github.io/kali24.html

HerrmannM 7y 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 7y ago
  Sure, look at [2]. I commented on your github repo too.
  - xorand 7y ago
    EDIT: Re: the chemistry, I do think that it might be a big subject, see https://arxiv.org/abs/1811.04960 https://arxiv.org/abs/1811.04960 , which somehow is not very surprising because of the Algorithmic Chemistry (aka ALCHEMY) of Fontana and Buss.

danharaj 7y 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 7y 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 7y ago

Does it have monads?

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