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.


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.