3 ms·

Teaching prolog in the context of modern type systems might be more worthwhile, since to my understanding, there's quite a bit of overlap, to where you can writ

Teaching prolog in the context of modern type systems might be more worthwhile, since to my understanding, there's quite a bit of overlap, to where you can write arbitrary prolog in Haskell or Scala's type systems. Probably even holds for C++ and TypeScript too. But I don't think there's a technological solution for teaching a subject for which the school cares so little that it won't hire anyone who actually understands it.

klodolph 1y ago
“Arbitrary prolog in Haskell’s type system” is overselling it. There are a lot of GHC extensions out there, so maybe some combination of extensions can bring this statement closer to reality. But, as stated, it’s pretty far away. There’s an important common thread shared by Prolog and type certain systems, which is unification, but Prolog gives you a lot of tools to control what happens when you go forward and backward: +---+ >---| |---> | | <---| |---< +---+ Prolog is, after all, Turing complete by design. I don’t know if Haskell’s type system is Turing complete with enough GHC extensions enabled, but if it is, then it’s by accident.
- syrak 1y ago
  You need very little to make a Prolog-like language Turing-complete (lists and recursive predicates). And so Haskell's type system only needs one (or two) extensions to be Turing-complete, `UndecidableInstances` (and maybe `FlexibleInstances` or `MultiParamTypeClasses`). It is no accident. The name "undecidable" shows that the authors of that extension were well aware that it enables Turing-completeness.
  - klodolph 1y ago
    Exactly—Haskell’s type checker can be made Turing-complete, but that won’t make it much like Prolog.
- fc417fc802 1y ago
  I'm not sure how useful it is in practice but even C++ templates are turing complete. https://rtraba.com/wp-content/uploads/2015/05/cppturing.pdf https://rtraba.com/wp-content/uploads/2015/05/cppturing.pdf > I don’t know if Haskell’s type system is Turing complete with enough GHC extensions enabled, but if it is, then it’s by accident. Undecidable instances? I don't think that's an accident. https://stackoverflow.com/questions/42356242/how-can-undecidable-instances-actually-hang-the-compiler https://stackoverflow.com/questions/42356242/how-can-undecid... Also see. https://github.com/seliopou/typo https://github.com/seliopou/typo
- chuckadams 1y ago
  True, I'm not sure you're going to get anything like cuts in a type system. I know with Haskell (GHC really, but that's kind of a given these days) and C++ you can make matching abort early, but only with an error.
jjtheblunt 1y ago
> since to my understanding, there's quite a bit of overlap, to where you can write arbitrary prolog in Haskell or Scala's type systems. Where did you get that idea? (I’m not seeing how that would work.)
- chuckadams 1y ago
  Repeating verbatim a post on a Haskell forum, someone talking about the Curry-Howard-Lambek correspondence and saying "you can write arbitrary Prolog in Haskell types". Seems most advanced type systems are already Turing-complete and based on unification matching, so I didn't see much reason to disbelieve it, though I realize that might be a little oversold. Obviously it doesn't look like Prolog, and you don't necessarily even want the Turing-completeness in your type system -- or at least not to have to rely on it anyway. But I still think the parallels are clear enough that it'd make for a pretty relevant piece of a course in logic programming.
  - pyrale 1y ago
    There is a blog post by Aphyr doing just that (typing the technical interview), which is well worth a read. That being said, it is a very small subset of what prolog does, and it has little practical use beyond writing a blog post.
pyrale 1y ago
Prolog and haskell communities are pushing in very different directions, and just because one piece in the haskell compiler happens to do one thing that prolog does, doesn’t mean haskell users get exposed to prolog ideas, or even that said piece of software offers a good way to express problems like prolog does. Sure, you could use haskell to express your problem as a type, aphyr style. You could also try to teach haskell concepts by having students write a haskell compiler in python. You could also write arbitrary prolog in brainfuck if you’re obstinate enough.

klodolph 1y ago

“Arbitrary prolog in Haskell’s type system” is overselling it. There are a lot of GHC extensions out there, so maybe some combination of extensions can bring this statement closer to reality. But, as stated, it’s pretty far away. There’s an important common thread shared by Prolog and type certain systems, which is unification, but Prolog gives you a lot of tools to control what happens when you go forward and backward: +---+ >---| |---> | | <---| |---< +---+ Prolog is, after all, Turing complete by design. I don’t know if Haskell’s type system is Turing complete with enough GHC extensions enabled, but if it is, then it’s by accident.

syrak 1y ago
You need very little to make a Prolog-like language Turing-complete (lists and recursive predicates). And so Haskell's type system only needs one (or two) extensions to be Turing-complete, `UndecidableInstances` (and maybe `FlexibleInstances` or `MultiParamTypeClasses`). It is no accident. The name "undecidable" shows that the authors of that extension were well aware that it enables Turing-completeness.
- klodolph 1y ago
  Exactly—Haskell’s type checker can be made Turing-complete, but that won’t make it much like Prolog.
fc417fc802 1y ago
I'm not sure how useful it is in practice but even C++ templates are turing complete. https://rtraba.com/wp-content/uploads/2015/05/cppturing.pdf https://rtraba.com/wp-content/uploads/2015/05/cppturing.pdf > I don’t know if Haskell’s type system is Turing complete with enough GHC extensions enabled, but if it is, then it’s by accident. Undecidable instances? I don't think that's an accident. https://stackoverflow.com/questions/42356242/how-can-undecidable-instances-actually-hang-the-compiler https://stackoverflow.com/questions/42356242/how-can-undecid... Also see. https://github.com/seliopou/typo https://github.com/seliopou/typo
chuckadams 1y ago
True, I'm not sure you're going to get anything like cuts in a type system. I know with Haskell (GHC really, but that's kind of a given these days) and C++ you can make matching abort early, but only with an error.

jjtheblunt 1y ago

> since to my understanding, there's quite a bit of overlap, to where you can write arbitrary prolog in Haskell or Scala's type systems. Where did you get that idea? (I’m not seeing how that would work.)

chuckadams 1y ago
Repeating verbatim a post on a Haskell forum, someone talking about the Curry-Howard-Lambek correspondence and saying "you can write arbitrary Prolog in Haskell types". Seems most advanced type systems are already Turing-complete and based on unification matching, so I didn't see much reason to disbelieve it, though I realize that might be a little oversold. Obviously it doesn't look like Prolog, and you don't necessarily even want the Turing-completeness in your type system -- or at least not to have to rely on it anyway. But I still think the parallels are clear enough that it'd make for a pretty relevant piece of a course in logic programming.
- pyrale 1y ago
  There is a blog post by Aphyr doing just that (typing the technical interview), which is well worth a read. That being said, it is a very small subset of what prolog does, and it has little practical use beyond writing a blog post.

pyrale 1y ago

Prolog and haskell communities are pushing in very different directions, and just because one piece in the haskell compiler happens to do one thing that prolog does, doesn’t mean haskell users get exposed to prolog ideas, or even that said piece of software offers a good way to express problems like prolog does. Sure, you could use haskell to express your problem as a type, aphyr style. You could also try to teach haskell concepts by having students write a haskell compiler in python. You could also write arbitrary prolog in brainfuck if you’re obstinate enough.