The topic of functional logic programming is extraordinarily rich and is largely unexplored, due to limits of the original reasoning model (closed world SLD resolution) which hindered a view of the bigger picture.

David McAllester wrote all down in 1989 with Ontic, but it wasn’t recognized as being implementable nor was it even clearly understood what an implementation would comprise, nor were its connections to functional logic recognized.

Such a language so expressively mixes types and values that traditional type checking is inapplicable. The only tool adequate for compile-time reasoning is a static analysis of the program under the assumptions proffered by the domains of functions within it.

Because functional logic intermixes evaluation and potential failure, assumptions must be guarded by contingent term evaluations whose potential success determines the strength of the assumption, preserving order-independent confluence.

Which, modulo conventions and notations, is the inference rule part of an automated theorem prover. So we’ve come full circle from reasoning to programming and back, with a language model that is significantly more expressive than what we’re accustomed to.

I think this will be the hot topic for programming language research and implementation in the 2020’s by way of the 1980’s. The other fields have pushed to near the limits of their non-backtracking, non-orthogonal failure, separate-types-and-failures paradigms.

“But you can do full delimited functional logic evaluation in a Monad”, the Haskell programmers will say. Yes, but you can’t reason about its behavior that way.

“But we can’t unify (solve for the equality of) functions” is a leading argument against this model. But with some extensions to McAllester’s work, we can move that problem from unification to composing functions and checking the properties of the function.