`Maybe Monad`type (covered in this blog in May) is a practical data type in Haskell and is used extensively. Since it is also a

`MonadPlus`type, it is also immediately useful for logic programming, particularly of the semideterministic variety. Personal, I view

`Maybe`as a second-order

`Bool`ean type, which, in itself, is a very powerful mode of expression, as George Boole demonstrated. Do yourself a favor, reread his works on algebra, or perhaps some musings from others, such as Dijkstra. Just as Donald Knuth showed that any n-tree could be transformed into an equivalent binary tree, and Paul Tarau put that to good,

*ahem*, clause and effect, the Boolean algebra can model many other forms of algebras ... and does, for, after all, last I checked all my calculations are reduced to boolean representations (some call them

*bi*nary digi

*ts*).

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:

dataWhateverx =Onlyx |Anything

Just like

`Mabye`,

`Whatever`can be monadic:

instanceFunctor Whateverwheref (

fmapOnlyx) =Only(f x)

fmapfAnything=Anythinginstancex =Monad Whateverwhere

returnOnlyx

Onlyx >>= 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 ...

instanceEqx ⇒Eq(Whateverx)where

Onlyx ≡Onlyy = 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 ...

dataMan=Smith|Jones|Brownderiving (Eq,Show)dataPosition=Cashier|Manager|Tellerderiving (Eq,Show)typeSibling=BooltypeAns= (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

`Position`s ...

-- first rule definition: The teller must be an only child

sibling ::Position→Whatever Sibling

siblingTeller=Only False

sibling _ =Anything

-- fact: Brown has a sibling

hasSibling ::Man→Whatever Sibling

hasSiblingBrown=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-upguard

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.

ifpos1 ≡ pos2 ∨ man1 ≡ man2then[]

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 unification^{2}to find Smith

letk =const^{3}

letsmith = (second $ kSmith)∈[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 seed`

The 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 = ` When `x` is atomic, of course `f ≡ ` , 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. |

## 7 comments:

I hope you are aware than cyan text on white is almost invisible, especially for people with colour-blindness in red.

I propose a shorter keyword: Meh.

> hasSibling :: Teller → Whatever Sibling

You have a mistake there, should be Man -> Whatever Sibling

Enjoyable reading. Have you seen the LogicT monad transformer? http://okmij.org/ftp/Computation/monads.html#LogicT

I haven't done very much logic programming, but I think if I did, I'd do it in Haskell with LogicT.

@david, thanks for the fix ... yes, that was an error in the transcription of the Haskell source to the blog. Fixed it on the blog.

@denis, yes, I have reviewed LogicT and worked with it a bit. Not my cup of tea, so I've been working entirely within Haskell (arrows, monads, data types, and recently comonads) to get typeful logic programming and all of Haskell at any point in the program. My experiments so far have been promising: efficient runtime results and compact and consistent syntax. Still working on my system, as these blog entries demonstrate, so let me know how your explorations with LogicT go.

@barry, as we discussed off line, the cyan font colour is now darkened to stand out better from the white background.

Post a Comment