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…
polairscience 3 hours ago [-]
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.
I have written stuff in Prolog, but I find this lambda Prolog syntax very difficult to grok.
neuroelectron 3 hours ago [-]
So brainfuck x lisp
big-chungus4 27 minutes ago [-]
when I downloaded the example programs, they open up in my music player but don't play anything
big-chungus4 28 minutes ago [-]
(1987)
TheRoque 4 hours ago [-]
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.
pjmlp 4 hours ago [-]
First of all, it helps to actually use a proper compiled Prolog implementation like SWI Prolog.
Second you really need to understand and fine tune cuts, and other search optimization primitives.
Finally in what concerns Game AIs, it is a mixture of algorithms and heuristics, a single paradigm language (first order logic) like Prolog, can't be a tool for all nails.
laksjhdlka 4 hours ago [-]
With λProlog in particular I think it probably finds most of its use in specifying and reasoning about systems/languages/logics, e.g. with Abella. I don't think many people are running it in production as an implementation language.
OneDeuxTriSeiGo 2 hours ago [-]
Yeah the main use of it is probably in ELPI which is a higher order structural reasoning and AST transform tool for Coq/Rocq.
ux266478 3 hours ago [-]
> It's a really weird language to reason with IMO
I know you likely mean regular Prolog, but that's actually fairly easy and intuitive to reason with (code dependent). Lambda Prolog is much, much harder to reason about IMO and there's a certain intractability to it because of just how complex the language is.
anonzzzies 4 hours ago [-]
λProlog or Prolog? Probably Prolog I guess?
TheRoque 2 hours ago [-]
My bad. Was regular prolog yeah
wbolt 3 hours ago [-]
No. It is actually λProlog which seems to be an extension of Prolog.
anonzzzies 3 hours ago [-]
I was responding to @TheRoque GP; I know λProlog quite well and I would be pleasantly surprised if they saw that in university, but I think they got taught Prolog. If you mean to say that they saw Lambda Prolog and it is therefor a lot more popular than I believed it to be, then excellent and ignore this reply.
ux266478 3 hours ago [-]
Not at all, it's a completely different language with a very different computational foundation. It's an SML-Haskell type situation.
yodsanklai 4 hours ago [-]
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.
acjohnson55 3 hours ago [-]
Why do you think that?
yodsanklai 1 hours ago [-]
Because the type system gives you correctness properties, and gives fast feedback to the coding agent. Much faster to type check the code than let say write and run unit tests.
One possible disadvantage of static types is that it can make the code more verbose, but agents really don't care, quite the opposite.
butokai 48 minutes ago [-]
Funnily enough, when programming with agents in statically typed languages I always find myself in need of reminding the agent to check for type errors from the LSP. Seems like it's something they're not so fond of.
Rendered at 17:04:38 GMT+0000 (Coordinated Universal Time) with Vercel.
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…
https://www.lix.polytechnique.fr/
[1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...
Second you really need to understand and fine tune cuts, and other search optimization primitives.
Finally in what concerns Game AIs, it is a mixture of algorithms and heuristics, a single paradigm language (first order logic) like Prolog, can't be a tool for all nails.
I know you likely mean regular Prolog, but that's actually fairly easy and intuitive to reason with (code dependent). Lambda Prolog is much, much harder to reason about IMO and there's a certain intractability to it because of just how complex the language is.
One possible disadvantage of static types is that it can make the code more verbose, but agents really don't care, quite the opposite.