Comment by YeGoblynQueenne

Curry is very recognisably the functional programmer's conception of what logic programing is, which is the way it's described in the SICP book. Nothing to do with Resolution, Horn clauses, or even unification, instead it's all about DFS with backtracking. Sometimes dictionaries (!) have something to do with it [1].

I'm speaking from personal experience here. DFS with backtracking has always featured very prominently in discussions I've had with functional programming folks about logic programming and Prolog and for a while I didn't understand why. Well it's because they have an extremely simplified, reductive model of logic programming in mind. As a consequence there's a certain tendency to dismiss logic programming as overly simplistic. I remember a guy telling me the simplest exercise in some or other of the classic functional programming books is implementing Prolog in (some kind of) Lisp and it's so simple! I told him the simplest exercise in Prolog is implementing Prolog in Prolog but I don't think he got what I meant because what the hell is a Prolog meta-interpreter anyway [2]?

I've also noticed that functional programmers are scared of unification - weird pattern matching on both sides, why would anyone ever need that? They're also freaked out by the concept of logic varibles and what they call "patterns with holes" like [a,b,C,D,_,E] which are magickal and mysterious, presumably because you have to jump through hoops to do something like that in Lisp. Like you have to jump through hoops to treat your code as data, as you say.

And of course if you drop Resolution, you drop SLD-Resolution, and if you drop SLD-Resolution you drop the Horn clauses, whose big advantage is that they make SLD-Resolution a piece of cake. Hence the monstrous abomination of "logic programming" languages that look like ... Haskell. Or sometimes like Scheme.

Beh, rant over. It's late. Go to sleep grandma. yes yes you did it all with Horn clauses in your time yadda yadda...

___________

[1] Like in this MIT lecture by H. Abelson, I believe with G. Sussman looking on:

https://youtu.be/rCqMiPk1BJE?si=VBOWeS-K62qeWax8

[2] It's a Prolog interpreter written in Prolog. Like this:

  prove(true):-
    !. %OMG
  prove((Literal,Literals):-
    prove(Literal)
   ,prove(Literals).
  prove(Literal):-
    Literal \= (_,_)
   ,clause(Literal,Body)
   ,prove(Body).

Doubles as a programmatic definition of SLD-Resolution.