Logic programming fails for many reasons; interestingly it fails to integrate
with imperative programming or export its constructs. Haskell's monadic
I/O—explicitly passing a RealWorld
—offers a nice demonstration.
In a language such as Curry, functions are nondeterministic; a result is returned for each clause matched. Thus the famous
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = insert (perm xs)
where insert ys = x : ys
insert (y:ys) = y : insert ys
returns all permutations on a list, viz.
> perm [1,2,3]
[3,2,1]
[3,1,2]
[2,3,1]
[2,1,3]
[1,3,2]
[1,2,3]
Functional programming corresponds to intuitionistic logic, which restricts the right side of sequents and thence creates an asymmetry between questions and answers. Logic programming partially restores the status of questions; consider:
Prelude> 0?1?2?3
0
1
2
3
Prelude> x=:=(0?1?2?3) & x+x=:=x*x where x free
{x=0} True
{x=2} True
Let us pause to consider how I/O works in Haskell (and Curry):
newtype IO a = IO (RealWorld -> (a, RealWorld))
One passes around an abstract token representing the RealWorld
when performing
effects (such as memory writes, allocations in C). However, one must be careful. As Wadler points out, the RealWorld
must not be duplicated (or thrown away).
This destroys the promise of nondeterminism.
Prelude> putStrLn ("hi"?"hello")
hi
hello
ERROR: non-determinism in I/O actions occurred!
Curry objects to buggy programs; trying to solve for I/O actions (such as writing to an array) would just not work—fanning out and then pruning results would perform all the effects before refinement. Not only does nondeterminism recklessly duplicate the real world, constraints destroy the real world.
Let us remark that Haskell's approach of putting all effects in the I/O monad has an unseemly edge: randomness (for instance) can be duplicated; imagine
newtype Rand a = Rand (Seed -> (a, Seed))
This would be amenable to logic programming where IO
would not.
This is a legitimate distinction in effects systems for functional programming—whether the token type being passed around is linear.
Conclusion
Kell argues that C succeeds partly because it is communicative. Haskell remarkably succeeds in integrating with C, able to import C functions and work with them on its own terms. Logic programming, however, is hopeless. It cannot deal with imperative constructs on its own terms, for deep reasons rooted in logic.
Linear logic programming is very interesting in this light; linear logic does
not restrict the right side of sequents (as in intuitionistic logic), and unlike
classical logic we can prohibit profligacy in the RealWorld
.