I remember learning it in univerisity. It's a really weird language to reason with IMO. But really fun. However I've heard the performances are not that good if you wanna make e.g. game AIs with it.
I'm curious to see how AI is going to reshape research in programming languages. Statically typed languages with expressive type systems should be even more relevant for instance.
Constantly amused by the split in comments of any moderately innovative language post between ‘I don't care about all this explanation, just show me the syntax!’ and ‘I don't understand any of this syntax, what a useless language!’
If the language is ‘JavaScript but with square brackets instead of braces’ maybe the syntax is relevant. But in general concrete syntax is the least interesting (not least important, but easiest to change) thing in a programming language, and its similarity to other languages a particular reader knows less interesting still. JavaScript is not the ultimate in programming language syntax (I hope!) so it's still worth experimenting, even if the results aren't immediately comprehensible without learning.
In Prolog the syntax is incredibly important. It is designed to be metainterpreted with the same ease in which a for-loop might be written in another language.
This can be arbitrarily extended in very interesting, beautiful, and powerful ways. This is extraordinarily hard to achieve and did not happen by accident.
As a challenge, see how easy it is to write a metainterpreter in another language of your choice. Alternately, see if you can think of any way the metainterpretation system in Prolog could be improved.
Finally, think of what would happen to this if we changed the syntax and introduced something like object.field notation.
So while logical programming can be achieved with other syntaxes, the metaintrepretive aspect will be lost. I have yet to see a language that does this better.
Nice link, thank you! I'm not sure it's super related to my comment but it is closely related to some other things I'm thinking about. I'll give it a read :)
I think that might be my favorite department/lab website I've ever come across. Really fun. Doesn't at all align with the contemporary design status quo and it shows just how good a rich website can be on a large screen. Big fan.
A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality.
To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general.
So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference?
And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared?
Fun to poke at, maybe just enough modern interest in logic programming to get there too…
I did a few days of AoC in 2020 in λProlog (as a non-expert in the language), using the Elpi implementation. It provides a decent source of relatively digestable toy examples: https://github.com/shonfeder/aoc-2020
(Caveat that I don't claim to be a λProlog or expert.)
All examples showcase the typing discipline that is novel relative to Prolog, and towards day 10, use of the lambda binders, hereditary harrop formulas, and higher order niceness shows up.
Did some modest development on Lambda Prolog back in 1999. I still have a vivid memory of feeling my brain expanding :) like rewiring how I approach programming and opening up new territory in my brain.
It might sound weird and crazy, but it quite literally blew my mind at the time !
19 comments
[ 3.1 ms ] story [ 44.8 ms ] thread[1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...
https://www.lix.polytechnique.fr/Labo/Dale.Miller/lProlog/fe...
If the language is ‘JavaScript but with square brackets instead of braces’ maybe the syntax is relevant. But in general concrete syntax is the least interesting (not least important, but easiest to change) thing in a programming language, and its similarity to other languages a particular reader knows less interesting still. JavaScript is not the ultimate in programming language syntax (I hope!) so it's still worth experimenting, even if the results aren't immediately comprehensible without learning.
https://www.metalevel.at/acomip/
This can be arbitrarily extended in very interesting, beautiful, and powerful ways. This is extraordinarily hard to achieve and did not happen by accident.As a challenge, see how easy it is to write a metainterpreter in another language of your choice. Alternately, see if you can think of any way the metainterpretation system in Prolog could be improved.
Finally, think of what would happen to this if we changed the syntax and introduced something like object.field notation.
So while logical programming can be achieved with other syntaxes, the metaintrepretive aspect will be lost. I have yet to see a language that does this better.
https://www.lix.polytechnique.fr/
https://www.proquest.com/openview/2a5f2e00e8df7ea3f1fd3e8619...
A few of my own experiments in this time with unification over the binders as variables themselves shows there’s almost always a post HM inference sitting there but likely not one that works in total generality.
To me that spot of trying to binding unification in higher order logic constraint equations is the most challenging and interesting problem since it’s almost always decidable or decidably undecidable in specific instances, but provably undecidable in general.
So what gives? Where is this boundary and does it give a clue to bigger gains in higher order unification? Is a more topological approach sitting just behind the veil for a much wider class of higher order inference?
And what of optimal sharing in the presence of backtracking? Lampings algorithm when the unification variables is in the binder has to have purely binding attached path contexts like closures. How does that get shared?
Fun to poke at, maybe just enough modern interest in logic programming to get there too…
(Caveat that I don't claim to be a λProlog or expert.)
All examples showcase the typing discipline that is novel relative to Prolog, and towards day 10, use of the lambda binders, hereditary harrop formulas, and higher order niceness shows up.
It might sound weird and crazy, but it quite literally blew my mind at the time !
I personally found it by asking for a specific language recommendation from ChatGPT, and one of the suggestions was Prolog.