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?
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.
It is still nice, but you need to manage the context yourself (eg represent it as a list, pass it around, ...)
This pearl is also an interesting read https://media.githubusercontent.com/media/astampoulis/makam-paper-funpearl/master/published.pdf
Last updated: Jun 06 2023 at 22:01 UTC