Yes, Maybe's all well and good (and for the most part, it is — it's very well-suited to describe a large class of problems). But, as a dyed-in-the-wool logic programmer, Haskell has a bit of a nagging problem capturing the concept of logic variables ... that is, a thing that either may be grounded to a particular value (which Maybe already has when the instance is Just
x) or may be free (which Maybe does not have). In short, the problem is with Nothing. And what is the problem? Values resolving to Nothing in a monadic computation, because they represent mzero, or failure, propagate throughout the entire (possibly chained) computation, forcing it to abort. Now, under the Maybe protocol, this is the desired result, but, when doing logic programming, it is often desirable to proceed with the computation until the value is grounded.Now, deferred computation in Haskell is not a novel concept. In fact, there are several approaches to deferred, or nondeterministic, assignment, including my own unification recipe as well as the credit card transformation (which the author immediately disavows). The problem with these approaches is that they require resolution within that expression. What we need is a data type that captures succinctly this decided or undecided state. This we do with the Whatever data type:
data Whatever x = Only x | Anything
Just like Mabye, Whatever can be monadic:
instance Functor Whatever where
fmap f (Only x) = Only (f x)
fmap f Anything = Anything
instance Monad Whatever where
return x = Only x
Only x >>= f = f x
Anything >>= f = Anything
You'll note that the monadic definition of Whatever is the same as Maybe, with the exception that Maybe defines
fail on Nothing, whereas Whatever has no such semantics.Even though Whatever is monadic, the interesting properties of this data type come to the fore in its more ordinary usage ...
instance Eq x ⇒ Eq (Whatever x) where
Only x ≡ Only y = x ≡ y
Anything ≡ _ = True
_ ≡ Anything = True
... and with that definition, simple logic puzzles, such as the following, can be constructed:
In a certain bank the positions of cashier, manager, and teller are held by Brown, Jones and Smith, though not necessarily respectively.
The teller, who was an only child, earns the least.
Smith, who married Brown's sister, earns more than the manager.
What position does each man fill?1
An easy enough puzzle solution to construct in Prolog, I suppose, and now given the Whatever data type, easy enough in Haskell, too! Starting from the universe of pairs that contain the solution ...
data Man = Smith | Jones | Brown deriving (Eq, Show)
data Position = Cashier | Manager | Teller deriving (Eq, Show)
type Sibling = Bool
type Ans = (Position, Man)
universe :: [Ans]
universe = [(pos, man) | pos ← [Cashier, Manager, Teller],
man ← [Smith, Jones, Brown]]
... we restrict that universe under the constraint of the first rule ("The teller, who was an only child...") by applying "only child"ness to both the Teller and to the Man holding that Position (as obtained from the fact: "... Brown's sister ..."), but, importantly, abstaining from defining a sibling restriction on the other Positions ...
-- first rule definition: The teller must be an only child
sibling :: Position → Whatever Sibling
sibling Teller = Only False
sibling _ = Anything
-- fact: Brown has a sibling
hasSibling :: Man → Whatever Sibling
hasSibling Brown = Only True
hasSibling _ = Anything
-- seed: the universe constrained by the sibling relation
seed :: [Ans]
seed = filter (λ(pos, man).sibling pos ≡ hasSibling man) universe
And, given that, we need define the rest of the rules. The first implied rule, that each Position is occupied by a different Man is straightforward when implemented by the
choose monadic operator defined elsewhere, the other rule concerns the pecking order when it comes to earnings: "The teller ... earns the least" (earnings rule 1) and "Smith, ..., earns more than the manager." (earnings rule 2). This "earnings" predicate we implement monadically, to fit in the domain of choose ...-- the earnings predicate, a suped-up guard
makesLessThan :: Ans → Ans → StateT [Ans] [] ()
-- earning rule 1: the teller makes less than the others
(Teller, _) `makesLessThan` _ = StateT $ λans. [((), ans)]
_ `makesLessThan` (Teller, _) = StateT $ λ_. []
-- and the general ordering of earnings, allowed as long as it's
-- different people and positions
(pos1, man1) `makesLessThan` (pos2, man2) = StateT $ λans.
if pos1 ≡ pos2 ∨ man1 ≡ man2 then []
else [((), ans)]
... we then complete the earnings predicate in the solution definition:
rules :: StateT [Ans] [] [Ans]
rules = do teller@(Teller, man1) ← choose
mgr@(Manager, man2) ← choose
guard $ man1 ≠ man2
cashier@(Cashier, man3) ← choose
guard (man1 ≠ man3 ∧ man2 ≠ man3)
-- we've extracted an unique person for each position,
-- now we define earnings rule 2:
-- "Smith makes more than the manager"
-- using my good-enough unification2 to find Smith
let k = const3
let smith = (second $ k Smith)∈[teller,mgr,cashier]
mgr `makesLessThan` smith
return [teller, mgr, cashier]
... and then to obtain the solution, we simply evaluate the
rules over the seed:evalStateT rules seedThe pivotal rôle that the Whatever data type is in the sibling relation (defined by the involuted darts
sibling and hasSibling). We can abduce the derived fact that Brown is not an only child, which, with this fact reduces the universe, removing the possibility that Brown may be a Teller ...universe \\ seed ≡ [(Teller,Brown)]... but what about the other participants? For Jones, when we are doing the
sibling/hasSibling involution, we don't know his familial status (we eventually follow a chain of reasoning that leads us to the knowledge that he is an only child) and, at that point in the reasoning we don't care. For Smith, we never have enough information derived from the problem to determine if he has siblings, and here again, we don't care. That is the power that the Whatever data type gives us,4 we may not have enough information reachable from the expression to compute the exact value in question, but we may proceed with the computation anyway. Unlike Maybe's resolution to one of the members of a type (Just x) or to no solution (Nothing), the Whatever data type allows the resolution (Only x), but it also allows the value to remain unresolved within the type constraint (Anything).5 So, I present to you, for your logic problem-solving pleasure, the Whatever data type.Endnotes
| 1 | Problem 1 from 101 Puzzles in Thought and Logic, by C. R. Wylie, Jr. Dover Publications, Inc. New York, NY, 1957. |
| 2 | f ∈ list = head [x|x ← list, f x ≡ x] When x is atomic, of course f ≡ id, but when x is a compound term, then there are many definitions for f for each data type of x that satisfy the equality f x ≡ x and that do not equate to id. We see one such example in the code above. |
| 3 | I really must define a library of combinators for Haskell, à la Smullyan's To Mock a Mockingbird, as I've done for Prolog. |
| 4 | This semantic is syntactically implement in Prolog as anonymous logic variables. |
| 5 | I find it ironic that Maybe says everything about the resolution of a value, but Whatever allows you to say Nothing about that value's resolution. |
