4 ms·

“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 t

“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.

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.