Stream: Elpi users & devs

Topic: Why did Elpi ended up looking like Elpi

walker (Dec 10 2022 at 17:55):

I understand the Elpi's goal is manipulating coq's AST:

my questions is why did elpi chose prolog as base language instead of something functional with total functions with ML style or with untotal function in haskel-like style?

Enrico Tassi (Dec 10 2022 at 19:30):

It chose lambdaProlog!
IMO it is the best to manipulate ASTs with binders, since the context is managed automatically. For this feature you need the program to be organized into rules, and that is the case in Prolog.

If you want to see the ideas behind lambdaProlog in a ML language look at MLTS.

Enrico Tassi (Dec 10 2022 at 19:31):

https://trymlts.github.io/

Enrico Tassi (Dec 10 2022 at 20:04):

It is still nice, but you need to manage the context yourself (eg represent it as a list, pass it around, ...)

Li-yao (Dec 11 2022 at 00:01):

This pearl is also an interesting read https://media.githubusercontent.com/media/astampoulis/makam-paper-funpearl/master/published.pdf

Last updated: Oct 13 2024 at 01:02 UTC