CMPUT 325 Schedule and Outcomes
14. Week 12 - Mar 31



14.1 Topics



14.2 More Monads

As strange as this may seem, monads are a way of imbedding an imperative language into your functional program. You almost always write monad code using the imperative-looking do statement, where you have <- assignment of variables to values from statements. The actual impertative language you are using, that is the way that "do" for a monad is interpreted, depends on how >>= is defined for the monad. For example The semantics of the particular imperative language is determined by the monad M. You can think of a value of type M a as a statement in the language M that returns a value of type a as result.

Now in an imperative language, the semicolon (;) can be thought of as the statement composition operation. A statement s is a function that takes the current state of the machine to the next state, that is next = s(current). So a sequence of statements
s1 ;
s2 ;
s3
can be thought of as a function composition applied to the current state
s3 (s2 (s1 (current))))
Here is a concrete example. If the program state is a pair (x,y), then a statement like x = x + 1 applied to (1,3) would be
(x = x + 1)(1, 3) = (2, 3)
So this program on initial state (1, 3)
x = x + 1;
y = y - 1;
x = x + y
becomes
(x = x + y) (y = y - 1) (x = x + 1) (1, 3) =
(x = x + y) (y = y - 1) (2, 3) =
(x = x + y) (2, 2) =
(4, 2)
If you don't supply the initial state, then you can just think in terms of function composition to get that
(x = x + y) (y = y - 1) (x = x + 1)
is the state transition function
\(x, y) -> (x+y, y-1)
The key idea here is that we need a rule for how to compose statements, and that rule depends on our language. We also need a way to extract out information from a statement for later use.

For a given monad M (think imperative language M), then you can think of M a as a statement in M that produces something of type a that can be used in later statements. So the bind operator >>=
(>>=) :: M a -> ( a -> M b ) -> M b
tells you how to sequence the statement M a followed by M b, given that M b might depend on the results computed by M a. And in fact in a do, where s2 might contain free occurrences of variable x
x <- s1;
s2

is the same as this outside of a do

s1 >>= (\x -> s2)
Now, we are still operating within a functional language, so you can only bind a variable once in its scope, so there can only be one instance of a variable on the left of a <-. So any imperative aspects similar to updating the value of a storage location will have to be done with explicit operations in the monad.

What about the badly named return? You can think of return as a function that constructs a statement in the monad that delivers the value supplied to the return. What happens next depends on the monad.

All monads must obey these laws:
right unit: m >>= return is equivalent to m
left unit: return x >>= f is equivalent to f x
associativity: (m >>= f) >>= g is equivalent to m >>= (\x -> f x >>= g)


14.3 The List Monad

Every statement in a list "program" generates a list. So even [1, 2] is a statement! Let's now make these ideas concrete. code/Week12/list1.hs

    import Control.Monad.State
     
    {-  
        List is a Monad with these operations:
     
        return x = [x]
        >>= :: [a] -> (a -> [b]) -> [b]
        xs >>= f = concat (map f xs)
     
        or using the concatMap = concat . map
        xs >>= f = concatMap f xs
     
        also note, since 
        m >> n = m >>= \_ -> n
        then 
        m >> n = concat (map (\_ -> n) m)
        which is length m copies of n
        
    -}
     
    {- with the definitions above, this -}
     
    ex1a = do 
        b1 <- [1, 2]
        b2 <- ["a", "b"]
        return (b1, b2)
     
    {- produces
        [(1,"a"),(1,"b"),(2,"a"),(2,"b")]
     
        Why is this?  In essence, a do over the list monad is a series of
        nested for loops, one for each variable on the lhs of <-
     
        To prove this, begin by converting to the use of >>=
    -}
     
    ex1b = 
      [1, 2] >>= \b1 ->
      ["a", "b"] >>= \b2 ->
      return (b1, b2)
     
    {- and then use the definition of >>= and return for lists 
     
    This amounts to mapping a function over a list, and concatenating the
    results.  This means the function being mapped must return a list.
    The function being mapped is itself a concat of a map over a list, so
    the inner function is returning a list.
     
    -}
     
    ex1c' = 
      [1, 2] >>= \b1 ->
          concat ( map (\b2 -> [ (b1, b2) ]) ["a", "b"] )
     
    ex1c = 
      concat (map (\b1 -> 
        concat ( map (\b2 -> 
            [ (b1, b2) ]) 
                ["a", "b"] ))  -- values of b2
                  [1, 2] ) -- values of b1
     
    {- 
    finally, this can also be written as a list comprehension, which is
    just syntactic sugar for the do, which is syntactic sugar for the >>=
    -}
     
    ex1d = [ (b1, b2) | b1 <- [1,2], b2 <- ["a", "b"] ]
     
    {- 
    now here is something a bit unexpected.  Every "statement" in the
    list monad program must generate a list.  So we can insert a
    statement into a program as follows: 
    -}
     
    ex1p s = do
        b1 <- [1, 2]
        -- observe what happens when you change s: [] [()] [1] [(), ()]
        s 
        b2 <- ["a", "b"]
        return (b1, b2)
     
    {- you get this:
     
        *Main> ex1p []
        []
     
        *Main> ex1p [1]
        [(1,"a"),(1,"b"),(2,"a"),(2,"b")]
     
        *Main> ex1p [()]
        [(1,"a"),(1,"b"),(2,"a"),(2,"b")]
     
        *Main> ex1p [(),()]
        [(1,"a"),(1,"b"),(1,"a"),(1,"b"),(2,"a"),(2,"b"),(2,"a"),(2,"b")]
     
    The reason this happens is because >> is defined as
        m >> n = concat (map (\_ -> n) m)
    so
        > map (\_ -> 1) []
        []
        > map (\_ -> 1) [()]
        [1]
     
    and so a sequence m >> n can be selectively interrupted or continued
    or even duplicated.
     
    You also get interesting things like this, remembering that return
    just generates a statement in the monad.
     
        *Main> [1, 2, 3] >>= return [4] >>= return [5]
        [5,5,5]
    -}
     
Let's verify that the list monad satisfies the monad laws. code/Week12/list1laws.hs

    import Control.Monad.State
     
    {-  
        List is a Monad with these operations:
     
        return x = [x]
        >>= :: [a] -> (a -> [b]) -> [b]
        xs >>= f = concat (map f xs)
     
        and it should satisfy these laws
     
        right unit: 
                m >>= return 
            is equivalent to 
                m
     
        left unit: 
                return x >>= f 
            is equivalent to 
                f x
     
        associativity: 
                (m >>= f) >>= g 
            is equivalent to 
                m >>= (\x -> f x >>= g) 
    -}
     
    {- with the definitions above, 
     
        note: m results in a list, say [e0, e1, ...]
     
        m >>= return
        concat (map return m)
        concat [ (return e0), (return e1), ... ]
        concat [ [e0], [e1], ... ]
        [e0, e1, ...]
        m
     
        note: operations f,g below have to result in a list
     
        return x >> f
        concat (map f (return x))
        concat (map f [x])
        concat [f x]
        f x
     
        (m >> f) >>= g
        concat (map g (m >> f))
        concat (map g (concat (map f m)))
     
        note: concat [ (map g L0), (map g L1), ... ]
        is the same as
              (map g (concat [ L0, L1, ... ]))
     
        m >> = (\x -> f x >>= g)
        m >> = (\x -> (concat (map g (f x))))
        (concat (map (\x -> (concat (map g (f x)))) m))
        (concat (map (\x -> (concat (map g (f x)))) [e0, e1, ...]))
     
        (concat [(concat (map g (f e0))), (concat (map g (f e1))), ...])
     
        f results in a list, g results in a list for element of the
        list from f, so we can collect all the f results first, and 
        then feed that list into g
     
        (concat (map g (concat (map f [e0, e1, ...]))))
        (concat (map g (concat (map f m))))
        (concat (map g (m >>= f))))
        (m >>= f) >>= g
     
    -}
     
    ex1a = do 
        b1 <- [1, 2]
        b2 <- ["a", "b"]
        return (b1, b2)
     
    ex1b = 
      [1, 2] >>= \b1 ->
      ["a", "b"] >>= \b2 ->
      return (b1, b2)
     
    ex2b = 
      [1, 2] >>= \b1 ->
      ["a", "b"] >>= 
      return >>= \b2 ->
      return (b1, b2)
     


14.4 Sequencing Monad Actions

code/Week12/sequence.hs

    {- What if you have a sequence of monad operations you want to perform.
    For example
     
        *Main> map print [1, 2,3 ]
     
        <interactive>:80:1:
            No instance for (Show (IO ())) arising from a use of `print'
            Possible fix: add an instance declaration for (Show (IO ()))
            In a stmt of an interactive GHCi command: print it
     
        *Main> :t map print [1, 2, 3]
        map print [1, 2, 3] :: [IO ()]
     
    produces a sequence of IO operations, but does not actually perform them.
     
    To actually do them, i.e evaluate each action in the sequence from left 
    to right, and collect the results, use the seqeunce operation:
     
        sequence :: Monad m => [m a] -> m [a]
        sequence ms = foldr k (return []) ms
            where
              k m m' = do { x <- m; xs <- m'; return (x:xs) }
     
    Examples:
        *Main> do sequence $ map print [1, 2, 3]
        1
        2
        3
        [(),(),()]
     
        *Main> do sequence $ map print [1, 2, 3]; return ()
        1
        2
        3
    -}
     
     


14.5 MonadPlus

Sometimes you want to combine the results of a number of monad computations. For example, find the first Maybe that is not Nothing, or make a list of all the computations that worked. So what "combine" means depends on your goals. code/Week12/listplus.hs

    import Control.Monad.State
    {-
     
        A MonadPlus is a way of combining the results of two monad computations.  
        What "combine" means depends on your goals and the particular monad.
        
        class Monad m => MonadPlus m where
            mzero :: m a
            mplus :: m a -> m a -> m a
     
        where for lists we have 
            instance MonadPlus [] where
                mzero = []
                mplus = (++)
     
        msum combines, under mplus, a list of monad computations
            msum :: MonadPlus m => [m a] -> m a
            msum = foldr mplus mzero
     
        guard blocks off a route
            guard :: MonadPlus m => Bool -> m ()
            guard True  = return ()
            guard False = mzero
     
        so for lists we have 
            guard True  = [()]
            guard False = []
        the guard command is like a break in a for loop
    -}
     
    {- 
        *Main> msum $ map (\x -> [[x]]) [1, 2, 3]
        [[1],[2],[3]]
     
        *Main> msum $ map (\x -> (if (x==2) then [] else [[x]])) [1, 2, 3]
        [[1],[3]]
     
        *Main> sequence $ map (\x -> [[x]]) [1, 2, 3]
        [[[1],[2],[3]]]
     
        *Main> sequence $ map (\x -> (if (x==2) then [] else [[x]])) [1, 2, 3]
        []
    }
     
    ex2a = do 
        b1 <- [1, 2, 3, 4]
        guard (b1 /= 2)
        b2 <- ["a", "b", "c"]
        guard (b2 /= "b")
        return (b1, b2)
     
    ex2a' = do 
        b1 <- [1, 2, 3, 4]
        if (b1 /= 2)
            then do 
                b2 <- ["a", "b", "c"]
                if ( b2 /= "b")
                then do
                    return (b1, b2)
                else do
                    []
            else do
                []
        
    {- so why should this work? For lists, it has to do with how a map of a 
    function that ignores its argument works:
        
    Note:
    > map (\_ -> 1) []
    []
    > map (\_ -> 1) [()]
    [1]
     
    So the guard returns the [] when false, so further maps are aborted.
    -}
     
    ex2b = 
      [1, 2, 3, 4] >>= \b1 ->
      guard(b1 /= 2) >> 
      ["a", "b", "c"] >>= \b2 ->
      guard (b2 /= "b") >> 
      return (b1, b2)
     
     
    ex2c' = 
      concatMap (\b1 -> 
        concatMap (\_ -> 
            concatMap (\b2 -> 
                concatMap (\_ -> [ (b1, b2) ]) 
                    (guard (b2 /= "b")) )
                        ["a", "b", "c"] )  -- values of b2
                          (guard (b1 /= 2)))   -- values of guard: [] or [()]
                              [1, 2, 3, 4] -- values of b1
     
    ex2c = 
      concat (map (\b1 -> 
        concat (map (\_ -> 
            concat ( map (\b2 -> 
                concat (map (\_ -> 
                    [ (b1, b2) ]) 
                        (guard (b2 /= "b")) ))
                        ["a", "b", "c"] ))  -- values of b2
                          (guard (b1 /= 2)) ))  -- values of guard: [] or [()]
                              [1, 2, 3, 4] ) -- values of b1
     
     
    {- Another example taken from 
        http://en.wikibooks.org/wiki/Haskell/MonadPlus
    -}
     
    pythags = do
      z <- [1..]
      x <- [1..z]
      y <- [x..z]
      guard (x^2 + y^2 == z^2)
      return (x, y, z)
     
    pythags1 =
      [1..] >>= \z ->
      [1..z] >>= \x ->
      [x..z] >>= \y ->
      guard (x^2 + y^2 == z^2) >>= \_ ->
      return (x, y, z)
     
    pythags2 =
     let ret x y z = [(x, y, z)]
         gd  z x y = concatMap (\_ -> ret x y z) (guard $ x^2 + y^2 == z^2)
         doY z x   = concatMap (gd  z x) [x..z]
         doX z     = concatMap (doY z  ) [1..z]
         doZ       = concatMap (doX    ) [1..]
     in doZ
     
     


14.6 Another Example

code/Week12/list3.hs

    {- 
        Given a list of tuples (Name, [ Values]) where values is a 
    [ String ] that gives all the allowable values of name, generate all
    possible assignments.  
    -} 
     
    type Name = String
    type Value = String
     
    {- generates all possible assignments -}
     
    -- monad version
    genA :: [ (Name, [Value]) ] -> [ [ (Name, Value) ] ]
    -- genA [ ]  = [ [] ]
    genA [ ]  = [ ]
    genA ( (n, vals):rest ) = do
        v <- vals
        o <- genA rest
        return ( (n, v) : o )
     
    -- list comprehension version
    genB :: [ (Name, [Value]) ] -> [ [ (Name, Value) ] ]
    genB [] = [ [] ]
    genB ( (n, vals):rest ) = [
        (n, v) : o |
        v <- vals,
        o <- genB rest
        ]
     
    a1 = [ ("a", ["0", "1"]), ("b", ["x", "y", "z"]) ]


14.7 Using the State Monad in Algorithms

code/Week12/tree.hs

    import Control.Monad.State
     
    {- A tree containing nodes of type a -}
    data Tree a = Leaf a | Node a (Tree a) (Tree a) deriving (Show, Eq)
     
    testTree = 
        Node "A" (Node "B" (Leaf "C" ) (Node "D" (Leaf "E") (Leaf "F"))) (Leaf "G")
     
    {- 
        Given a tree t, dfsLabelTree generates an isomorphic Tree Int that 
        has values that are the positions that the leaf or node is visited in
        a depth first searhc.
     
        The algorithm is expressed as a state monad, in which the state of
        the monad is the next dfs number to use.  The initial number is 0
     
        Note how
            *Main> :t dfsTree testTree 
            dfsTree testTree :: State Int (Tree Int)
     
        is a state monad, that is, a state machine program that is waiting to
        be run on an initial state.
     
    -}
     
    dfsTree :: Tree a -> State Int (Tree Int)
     
    dfsTree (Leaf x) = do
        n <- get
        put (n+1)
        return (Leaf n)
     
    dfsTree (Node x t1 t2) =  do 
        n <- get
        put (n+1)
        dt1 <- dfsTree t1
        dt2 <- dfsTree t2
        return (Node n dt1 dt2)
     
    {- your result depends on how you run the program resulting from dfsTree 
     
        prog = dfsTree testTree
        prog :: State Int (Tree Int)
     
        runState prog 0
        evalState prog 0
        execState prog 0
     
        result and the state
        *Main> runState prog 0
        (Node 0 (Node 1 (Leaf 2) (Node 3 (Leaf 4) (Leaf 5))) (Leaf 6),7)
     
        result only
        *Main> evalState prog 0
        Node 0 (Node 1 (Leaf 2) (Node 3 (Leaf 4) (Leaf 5))) (Leaf 6)
     
        state only
        *Main> execState prog 0
        7
    -}
     
    dfsLabelTree :: Tree a -> Tree Int
    dfsLabelTree t = evalState (dfsTree t) 0 
     
    {- if you want to label two trees, you can do this -}
    p1 = do 
        t1 <- dfsTree testTree; 
        t2 <- dfsTree testTree; 
        return (t1,t2)
     
    {- and get this output 
        *Main> evalState p1 0
        (Node 0 (Node 1 (Leaf 2) (Node 3 (Leaf 4) (Leaf 5))) (Leaf 6),
         Node 7 (Node 8 (Leaf 9) (Node 10 (Leaf 11) (Leaf 12))) (Leaf 13))
    -}
     
     
    {- 
        suppose you want to label the nodes in the tree with their path from
        the root.
    -}
     
    pathTree :: Tree a -> State [ Int ] (Tree [ Int ])
    pathTree (Leaf x) = do
        pRoot <- get
        return (Leaf pRoot)
     
    pathTree (Node x t1 t2) = do
        pRoot <- get
        put (pRoot ++ [0])
        pt1 <- pathTree t1
        put (pRoot ++ [1])
        pt2 <- pathTree t1
        return (Node pRoot pt1 pt2)
        
    path :: Tree a -> Tree [ Int ]
    path t = evalState (pathTree t) []


14.8 Sample Enchanced Solver

code/Week12/solverdemo.hs

    {- Constraint satisfaction solving
     
    Modifed from
     
    from http://www.haskell.org/haskellwiki/All_About_Monads#StateT_with_List 
     
    Background modules:
     
    http://www.haskell.org/haskellwiki/State_Monad
    http://www.cis.upenn.edu/~bcpierce/courses/advprog/resources/base/Control.Monad.State.html
     
    http://hackage.haskell.org/package/base-4.6.0.1/docs/Control-Monad.html
    https://hackage.haskell.org/package/mtl-2.0.1.0/docs/Control-Monad-State.html
     
     
    Here is a interesting example of combining the StateT monad with
    the List monad to produce a monad for stateful nondeterministic
    computations.
     
    We will apply this powerful monad combination to the task of
    solving constraint satisfaction problems (in this case, a logic
    problem). The idea behind it is to have a number of variables that
    can take on different values and a number of predicates involving
    those variables that must be satisfied. The current variable
    assignments and the predicates make up the state of the
    computation, and the non-deterministic nature of the List monad
    allows us to easily test all combinations of variable assignments.
     
    We start by laying the groundwork we will need to represent the
    logic problem, a simple predicate language:
     
    -}
    import Data.Maybe
    import Control.Monad
    import Control.Monad.State
    import Text.Printf
     
     
    {- pretty printer for models, display using putStrLn 
        Assumes that each model has variables in the same order in the
    list -}
     
    showModels :: [Variables] -> String
    showModels models = 
        show models
     
    {-
        A language to express logic problems
     
        Var are variables, named with strings
        Value are values of variables, values are strings
        Predicates are functions with values are true or false
    -}
     
    type Name   = String
    type Value = String
    type VarType = String
    data Predicate = 
                 Is    Name Value            -- var has specific value
               | Equal Name Name              -- vars have same (unspecified) value
               | And   Predicate Predicate  -- both are true
               | Or    Predicate Predicate  -- at least one is true
               | Not   Predicate            -- it is not true
      deriving (Eq, Show)
     
    type Variables = [(Name,Value)]
     
    -- derived predicates
     
    -- test for a variable NOT equaling a value
    isNot :: Name -> Value -> Predicate
    isNot var value = Not (Is var value)
     
    -- if a is true, then b must also be true
    implies :: Predicate -> Predicate -> Predicate
    implies a b = Not (a `And` (Not b))
     
    -- iff
    iff :: Predicate -> Predicate -> Predicate
    iff a b = (a `implies` b) `And` (b `implies` a)
     
    -- exclusive or
    orElse :: Predicate -> Predicate -> Predicate
    orElse a b = (a `And` (Not b)) `Or` ((Not a) `And` b)
     
    {-
        Check a predicate with the given variable bindings.
        An unbound variable causes a Nothing return value.
        otherwise you get Just True or Just False.
     
        lookup takes a list of name-value tuples, and returns the
        corresponding value Just v, or Nothing if name is not present.
     
        lookup :: Eq a => a -> [(a, b)] -> Maybe b
    -}
     
    check :: Predicate -> Variables -> Maybe Bool
    check (Is var value) vars = do val <- lookup var vars
                                   return (val == value)
    check (Equal v1 v2)  vars = do val1 <- lookup v1 vars
                                   val2 <- lookup v2 vars
                                   return (val1 == val2)
     
    {- 
        lifting takes a function (a1 -> r) and turns it into a function
        on monads (m a1 -> m r)
     
        liftM :: Monad m => (a1 -> r) -> m a1 -> m r
        liftM2 :: Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m rSource
     
    Promote a function to a monad, scanning the monadic arguments from
    left to right. For example, 
     
        liftM2 (+) [0,1] [0,2] = [0,2,1,3]
        liftM2 (+) (Just 1) Nothing = Nothing
    -}
     
    check (And p1 p2)    vars = liftM2 (&&) (check p1 vars) (check p2 vars)
    check (Or  p1 p2)    vars = liftM2 (||) (check p1 vars) (check p2 vars)
    check (Not p)        vars = liftM (not) (check p vars)
     
    {-
        Machinery for representing and solving constraint satisfaction
    problems.  This is where we will define our combined monad.
     
        ProblemState is the type of our logic problem.  Note the use of
    named fields where:
     
            vars is the environment, binding variables to values.   
            constraints are a collection of predicates that must be satisfied
                in order for an environment to be a solution. 
    -}
     
    data ProblemState = PS {vars::Variables, constraints::[Predicate]}
     
    -- this is our monad type for non-determinstic computations with state
    type NDS a = StateT ProblemState [] a
     
    -- lookup a variable in the environment.
    getVar :: Name -> NDS (Maybe Value)
    getVar v = do vs <- gets vars
                  return $ lookup v vs
     
    -- set a variable in the environment.
    setVar :: Name -> Value -> NDS ()
    setVar v x = do st <- get
                    vs' <- return $ filter ((v/=).fst) (vars st)
                    put $ st {vars=(v,x):vs'}
     
    {- 
    Check if the variable assignments satisfy all of the predicates.
    The partial argument determines the value used when a predicate
    returns Nothing because some variable it uses is not set.  Setting
    this to True allows us to accept partial solutions, then we can use
    a value of False at the end to signify that all solutions should be
    complete.
     
    Note:  maybe :: b -> (a -> b) -> Maybe a -> b
           (maybe x id) (Just y) = y
           (maybe x id) Nothing = x
    is the way you yield a default value
     
    Note:  (maybe x id) (Just y) = y
           (maybe x id) Nothing = x
    is the way you yield a default value
    -}
     
    isConsistent :: Bool -> NDS Bool
    isConsistent partial = do cs <- gets constraints
                              vs <- gets vars
                              let results = map (\p->check p vs) cs
                              return $ and (map (maybe partial id) results)
     
    {-
    Return only the variable bindings that are complete consistent
    solutions.  getFinalVars :: NDS Variables getFinalVars = do c <-
    isConsistent False guard c gets vars
    -}
     
    {-
     
    Get the first solution to the problem, by evaluating the solver
    computation with an initial problem state and then returning the
    first solution in the result list, or Nothing if there was no
    solution.
     
    -}
     
    getSolution :: NDS a -> ProblemState -> Maybe a
    getSolution c i = listToMaybe (evalStateT c i)
     
    {-
    Get a list of all possible solutions to the problem by evaluating
    the solver computation with an initial problem state.
    -}
     
    getAllSolutions :: NDS a -> ProblemState -> [a]
    getAllSolutions c i = evalStateT c i
     
    said :: Name -> Predicate -> Predicate
    said v p = ((v `Is` "knight") `implies` p) `And`
               ((v `Is` "knave") `implies` (Not p)) `And`
               ((v `Is` "normal") `implies` (p `Or` (Not p))) 
     
    {- lying is saying something is true when it isn't, or not saying
    anything -}
     
    lied :: Name -> Predicate -> Predicate
    lied v p = (v `said` p) `And` (Not p) 
     
    {- telling truth is saying something is true when it is, or not
    saying anything. -}
     
    toldTruth :: Name -> Predicate -> Predicate
    toldTruth v p = (v `said` p) `implies` p 
     
    -- Test consistency over all allowed settings of the variable.
     
    tryAllValues :: (Name,VarType) -> NDS ()
    tryAllValues (var,vtype) = do 
        -- try all the possible values of the type of var using
        -- lookupType :: VarType -> [ Value ]
        -- note the use of monad sum to put plus between each possibility
        msum $ map (setVar var) (lookupType vtype) 
        c <- isConsistent True
        guard c
     
    {- All that remains to be done is to define the puzzle in the
    predicate language and get a solution that satisfies all of the
    predicates: -}
     
     
    {- Define the problem, try all of the variable assignments and
    print a solution.  solve takes a set of constraints and returns a
    list of all the variable assignments that satisfy the constraints.
     
    Each call to tryAllValues will fork the solution space, assigning
    the named variable to be "knight" in one fork and "knave" in the
    other. The forks which produce inconsistent variable assignments
    are eliminated (using the guard function). The call to getFinalVars
    applies guard again to eliminate inconsistent variable assignments
    and returns the remaining assignments as the value of the
    computation.  
     
    if only asking for a few solutions, lazyness should stop further
    search
     
    -}
     
    solve :: [(Name,VarType)] -> [Predicate] -> [Variables]
    solve varOrder constraints = do 
                let variables   = []
                    problem     = PS variables constraints
     
                (getAllSolutions
                        (do 
                           sequence $ map tryAllValues varOrder
                           getFinalVars)
                         problem)   
     
    {- 
     
    We introduce types for the variables using a function lookupType
    that for each type gives the possible values it can have.
     
    The we identify the variables in the problem and their types, along
    with the order in which they should be searched, with the earliest
    variables being the most frequently changed (in model checking the
    order in which variables are examined can dramatically affect
    solution time).  
     
    -}
     
    lookupType :: VarType -> [ Value ]
    -- a generic person
    lookupType "Per" = ["knight", "knave", "normal" ]
    -- just knights and knaves
    lookupType "KK" = ["knight", "knave" ]
    -- paths are good or bad
    lookupType "Path" = ["good", "bad" ]
     
    varOrder = [ 
        ("B", "KK"),
        ("A", "KK"),
        ("R", "Path"),
        ("L", "Path")
        ]
     
    pSolve :: [Predicate] -> IO ()
    pSolve constraints = putStrLn (showModels $ solve varOrder constraints)
     
    {- Puzzles from notes -}
     
    {- there are 16 possible configurations that the situation can take
    when there are just knights and knaves.
    -}
     
    pU = [
        Not (Equal "A" "B"),
        Not (Equal "L" "R")
        ]
     
    {-
    Let's simplify by assuming just knights and knaves, only one of
    each type, and a good and bad path. The solver tells you that there
    are only these possible states in the world:
     
           L       R       A       B
         bad    good   knave  knight
        good     bad   knave  knight
         bad    good  knight   knave
        good     bad  knight   knave
     
    So, what questions could you ask that will identify the proper path
    to take when you don't know which of the 4 states above actually
    holds?
     
    For example, suppose you ask A: would you say 
        "If B says 'the left is good', then the left is indeed good"
    if A answers yes, then this is true:
           L       R       A       B
        good     bad  knight   knave
    and we can encode the yes answer to the question as:
        ("A" `said` (
            (("B" `said`  ("L" `Is` "good")) `implies` ("L" `Is` "good"))
        )),
    and we have one case of 4 covered when this problem has only one
    model.
     
    But if A answers no, then this is true of the possible models:
           L       R       A       B
         bad    good   knave  knight
        good     bad   knave  knight
         bad    good  knight   knave
     
    and you still don't know which path to take.  So you need to ask
    another question.  So you will have to make a series of calls to
    the solver, with different questions until you can narrow down the
    proper answer.  That decision process can of course be encoded in a
    function to which you supply the answers to the questions.
     
    This question, if you ask it of A (or B, symmetrically) 
    -}
     
    -- if this has a model, then go left
    p0 = [ 
        -- A says "If B says 'the left is good', then the left is good"
        ("A" `said` (
            (("B" `said`  ("L" `Is` "good")) `implies` ("L" `Is` "good"))
        )), 
        -- consistency check
        ("L" `Is` "good"),
     
        -- one is knight, one is knave
        Not (Equal "A" "B"),
        -- one is good, one is bad
        Not (Equal "L" "R")
        ]
     
    -- if A said no, if no model, then must be this
    p1 = [ 
        -- negation of previous, A didn't say that,
        Not ("A" `said` (
            (("B" `said`  ("L" `Is` "good")) `implies` ("L" `Is` "good"))
        )), 
        ("A" `Is` "knight"),
     
        -- one is knight, one is knave
        Not (Equal "A" "B"),
        -- one is good, one is bad
        Not (Equal "L" "R")
        ]
     
14. Week 12 - Mar 31
CMPUT 325 Schedule / Version 2.31 2014-04-04