Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

github.com

Post reply on HN
Print view View original

1–10 of 10 posts

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

#2

Post by xorand »

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

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

#3

Post by HerrmannM »

xorand wrote: post #2

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!

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

#5

Post by xorand »

HerrmannM wrote: post #3
xorand wrote: post #2

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 ne…

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

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

#6

Post by xorand »

xorand wrote: post #5
HerrmannM wrote: post #3

Earlier quoted context omitted.

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 ne…

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.

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

#8

Post by HerrmannM »

danharaj wrote: post #4

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

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

#10

Post by HerrmannM »

HerrmannM wrote: post #9
voldacar wrote: post #7

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.
Post reply on HN