I'll share an idea for a logic programming project that I've been brewing for quite some time (but never started working on)...
As you may know, the engine behind Prolog is based on the unification algorithm (finding substitution values for variables to make two patterns equal). The same algorithm is behind Hindley-Milner -style type inference algorithms.
I have been considering writing a compiler for a programming language that would do type inference indirectly in two steps. In the first step (a typical syntax tree walk), rather than doing the actual unification directly, a Prolog -style logic program would be emitted. In the second step, the logic program is evaluated which will result in the types for the program.
The advantage of this approach would be allowing function overloading (similarly to C++ or Java) informally without interfaces or type classes. This means that there will be ambiguous types for expressions, something which is quite hairy to implement using a H-M based classic type inference algorithm. If the final output has ambiguous types, it is a compile error in the source program.
This is just a crazy idea I've been brewing, but this would definitely be a nice use case for a Prolog -style logic programming language. In practice, it wouldn't probably be Prolog itself, because implementing similar languages is so much fun and writing the code to call an external Prolog interpreter is about as much trouble but a lot less fun.
Prolog certainly isn't your every day programming tool, but in some cases it's a really good tool to have. And learning logic programming is one of those ventures that will expand your horizons.
> The advantage of this approach would be allowing function overloading (similarly to C++ or Java) informally without interfaces or type classes.
I might be misunderstanding something, but how does this allow function overloading more than ordinary let-polymorphism? Functions can already have a type like, say, ∀a.a→Int. It's also quite common to do type inference in two steps where the first pass creates type variables and a list of constraints. The set of constraints are then passed to a unification algorithm, see e.g. http://www.seas.upenn.edu/~cis552/lectures/stub/FunTypes.htm....
In a classic Hindley-Milner type inference algorithm, you can't have a function "add(int, int) -> int" and "add(float, float) -> float". E.g. in Haskell, you'd need a type class for this.
Modern functional programming languages use a type inference algorithm more sophisticated than the original H-M algorithm which are more flexible than the original algorithm. The link you gave as an example is Haskell with a handful of language extensions related to the type checker - something entirely different to the H-M algorithm.
There can be other ways of implementing a similar type checker in a different manner, this was just a fun idea I came up with.
> Prolog does not have functions. It has functors/predicates.
I know.
I was talking about functions in the source language of the hypothetical compiler. The Prolog -style logic programs would be an internal data structure of that compiler.
It's easy to get confused when talking about compilers and interpreters because the source, target and host language concepts can get mixed up. Adding one or more intermediate languages to the mix doesn't help either. Either I was unclear or you didn't read my comment carefully enough :)
> I wonder if you could do this for something like Python
For something like Python, yes. For Python the language (as it currently is), no, not to the degree that I was talking about (ie. fully statically typed to enable compiling to native code).
But clever type inference algorithms for dynamic languages are a field of active research. Because static type information is the key to compiling fast code, a lot of the research going on in using type inference algorithms in fast JavaScript and other dynamic language runtimes.
At best, programming with a language using a clever type inference algorithm is almost as flexible as programming with a dynamic language - I wish there was more work going on in implementing nicer type inference -based static programming languages for the mainstream.
I was actually more thinking about at edit time - IDEs already do a limited about of inference about dynamic languages (e.g. PyCharm, and VS and JavaScript) - I was wondering about the benefits about having an interactive Prolog model able to make inferences about your application as you write it....
As you may know, the engine behind Prolog is based on the unification algorithm (finding substitution values for variables to make two patterns equal). The same algorithm is behind Hindley-Milner -style type inference algorithms.
I have been considering writing a compiler for a programming language that would do type inference indirectly in two steps. In the first step (a typical syntax tree walk), rather than doing the actual unification directly, a Prolog -style logic program would be emitted. In the second step, the logic program is evaluated which will result in the types for the program.
The advantage of this approach would be allowing function overloading (similarly to C++ or Java) informally without interfaces or type classes. This means that there will be ambiguous types for expressions, something which is quite hairy to implement using a H-M based classic type inference algorithm. If the final output has ambiguous types, it is a compile error in the source program.
This is just a crazy idea I've been brewing, but this would definitely be a nice use case for a Prolog -style logic programming language. In practice, it wouldn't probably be Prolog itself, because implementing similar languages is so much fun and writing the code to call an external Prolog interpreter is about as much trouble but a lot less fun.
Prolog certainly isn't your every day programming tool, but in some cases it's a really good tool to have. And learning logic programming is one of those ventures that will expand your horizons.
Finally, here's a logic programming interpreter I wrote some years ago for a class: https://github.com/rikusalminen/slolog/tree/master/example