-----
(1) Can you elaborate on what you mean by the type inferencer being identical to the interpreter? I see the type inferencer in Python in joy/utils/types.py. And I see your interpreter in Prolog -- but how does that do type inference?
Why am I interested in type inference? I wrote a shell interpreter in 19K lines of Python:
http://www.oilshell.org/release/0.6.pre8/metrics.wwz/line-co... (scroll to the end for line count)
I want to compile it to faster code, and that likely involves type inference in the style of PyPy or ShedSkin (which are both used in production).
Background: http://www.oilshell.org/blog/2018/03/04.html
My understanding is that global type inference for 19K lines of code might be out of reach in terms of speed? As far as I know type inference algorithms are exponential in the worst case. While I'm using a relatively small subset of Python, the type system may still be considered rich (classes with single inheritance, __call__, varargs, perhaps typed dictionaries.)
Do you think Prolog is feasible for this problem? Does it offer you help in terms of debugging and performance problems? Maybe I need some syntax for explicit annotation so I can "help" the backtracking succeed?
I am not exactly sure how it will work. But doing it in Prolog seems somewhat appealing, if I can "prototype" the type system. Though there is the practical problem of simply getting the types into Prolog and back out. I think I would have to generate a prolog program with at least one clause for every variable in my 19K line interpreter?
In any case, thanks for the links to your code. I will be looking at these further.
-----
(2) A recent comment from someone with considerable expertise says that backtracking search just doesn't come up that often:
https://www.reddit.com/r/ProgrammingLanguages/comments/9kb9z...
I seem to recall that Paul didn't just work with Mercury -- he worked on it -- and his Ph.D. work shows that: https://paul.bone.id.au/
I think type inference is a great example of where it DOES come up. But very few people implement type systems (and production type checkers are often in imperative languages like TypeScript, or occasionally OCaml with Hack).
Various types of scheduling may be another place, but I would also count that as a very small proportion of programming work.
Not to mention games, network programming, kernels, etc. I believe you're wildly overstating the applicability of Prolog. A program might have small subproblems that could be expressed in Prolog, but the entire program doesn't fit that paradigm.
Also, I also asked in that Reddit thread for "production" uses of Prolog, and I don't really see it. Erlang moved away from it for "engineering reasons", and they were one of the biggest advocates (I read Joe Armstrong's paper about prototyping Erlang in Prolog). Rust is maybe moving toward it, but they're probably using their own implementation and not an off-the-shelf Prolog interpreter.
I think Prolog ironically falls in the category as Forth (and Joy is not even as practical as Forth). It's incredibly expressive for some things, and it has generated many epiphanies. But if you try to use it in production, you eventually "fall off a cliff" for parts of the program that don't fit the model.
I experimented with both Forth and Joy a number of years ago, and have Manfred von Thun's papers printed out, sitting on my bookshelf. The quadratic formula was one small example of things that are awkward in stack languages, but I think there are others on a larger, architectural scale that are "dealbreakers".
The conclusion I came to about Forth/Joy was that they're worth learning but there's a reason they aren't used much in production. I will probably end feeling the same way about logic programming (like Paul does after 10 years of deep experience), but I still want to learn it for the reasons everyone says.