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.

[1]: https://www.lix.polytechnique.fr/~dale/lProlog/proghol/extra...

It might sound weird and crazy, but it quite literally blew my mind at the time !

https://www.lix.polytechnique.fr/

I personally found it by asking for a specific language recommendation from ChatGPT, and one of the suggestions was Prolog.