Here comes the example for a non-Maybe monad that can be used in guard
qualifiers. At first, I found it hard to contrive an example that does
not look too contrived, but now the example is about to convince me that
it makes sense to extend guard qualifiers from Maybe to a more general
class.
This message should work as a literate Haskell-1.4 file.
Heribert.
----------------------------------------------------------------------
\begin{code}
module GuardsTest where
import Maybe
\end{code}
I thought @choice@ would be a better name for the function called
@extract@ in my previous mail. The functionality is also a bit
different. Intuitively, @choice d m@ chooses a "member" of the monadic
value @m@ (in the sense that monads represent collections), and returns
the default value @d@ if @m@ happens to be the empty collection, i.e.,
@zero@. @MonadChoice@ is the class of monads that provide such a
@choice@ function:
\begin{code}
class (MonadPlus m) => MonadChoice m where
choice :: a -> m a -> a
\end{code}
Probably it makes sense to require the following properties:
choice d (return x) = x
choice d zero = d
choice d (m ++ n) = choice (choice d m) n
An instance declaration for @Maybe@ is straightforward. After all,
@Maybe@ was the monad that I wanted to generalize by @MonadChoice@.
An instance declaration for the list monad is also straightforward, but
it is not as "canonical" as in the @Maybe@ case: It chooses the first
member of the list, but it could also choose any other one.
\begin{code}
instance MonadChoice Maybe where
choice d m = maybe d id m
instance MonadChoice [] where
choice d [] = d
choice d (x:_) = x
\end{code}
Now comes the promised monad @STF@. It is a state transformer with the
possibility to fail. Note that all the methods for @STF@ are defined
using the corresponding methods of @Maybe@. Therefore we would, e.g.,
only need to replace @Maybe (b, a)@ by @[(b, a)]@ in the @newtype@
declaration to get a nondeterministic state transformer.
\begin{code}
newtype STF a b = STF (a -> Maybe (b, a))
unSTF (STF t) = t
-- By the way: Why isn't the following supported?
-- newtype STF a b = STF {unSTF :: a -> Maybe (b, a)}
instance Functor (STF a) where
map f (STF t) = STF (\s -> map (\(x, s) -> (f x, s)) (t s))
instance Monad (STF a) where
return x = STF (\s -> return (x, s))
STF t >>= f = STF (\s -> t s >>= \(x, s) -> unSTF (f x) s)
instance MonadZero (STF a) where
zero = STF (\s -> zero)
instance MonadPlus (STF a) where
STF t ++ STF u = STF (\s -> t s ++ u s)
\end{code}
Before we can make @STF@ a @MonadChoice@, we need know an initial state
and what to do with the final state. For this purpose we define a class
@InitialFinal@ that provides an initial value and a test for the final
value. Then in the instance declaration for @STF@, we can initialize the
state and perform the test on the final state.
\begin{code}
class InitialFinal c where
initial :: c
final :: c -> Bool
instance (InitialFinal a) => MonadChoice (STF a) where
choice d (STF t) = choice d [x | (x, s) <- t initial, final s]
\end{code}
We will now apply STF in an example:
- Let the state be a stack, represented as a list. The stack should be
empty in the beginning and the end, which is expressed by the instance
declaration for @InitialFinal@.
- We have @push@ and @pop@ operations for the stack. Note that @pop@
fails for an empty stack.
- @unaryOp@ and @binaryOp@ apply a unary or binary operation to the
topmost stack element(s) and push the result back to the stack.
\begin{code}
newtype Stack a = Stack [a]
instance InitialFinal (Stack a) where
initial = Stack []
final (Stack xs) = null xs
push :: a -> STF (Stack a) ()
push x = STF (\(Stack xs) -> return ((), Stack (x:xs)))
pop :: STF (Stack a) a
pop = STF (\(Stack xs) -> case xs of
[] -> zero
(x:xs) -> return (x, Stack xs))
unaryOp :: (a -> a) -> STF (Stack a) ()
unaryOp op = do x <- pop
push (op x)
binaryOp :: (a -> a -> a) -> STF (Stack a) ()
binaryOp op = do x <- pop
y <- pop
push (y `op` x)
\end{code}
Now we can define a function that performs a sequence of operations. The
state should be initialized automatically and the final state should be
checked automatically as well. Essentially this leads to an interpreter
for reverse polish notation. To make the example a bit more complex, we
try to apply the operations in reverse order if the normal order does
not work.
With the proposed new syntax we could write:
evaluate :: [STF (Stack a) b] -> a
evaluate ops | () <- sequence ops,
z <- pop = z
evaluate ops | () <- sequence (reverse ops),
z <- pop = z
Since this syntax is not yet supported, we translate it to monad
comprehensions and the @choice@ function according to the equivalence
(*) given below. The translation assumes a third equation
evaluate ops = error "evaluate"
and is slightly simplified because all equations have the same
irrefutable argument pattern @ops@.
\begin{code}
evaluate :: [STF (Stack a) b] -> a
evaluate ops = choice (error "evaluate")
([z | () <- sequence ops, z <- pop]
++
[z | () <- sequence (reverse ops), z <- pop])
\end{code}
To see that it works, we can apply @evaluate@ to some test inputs:
evaluate [push 7, push 4, binaryOp (-)] -- 3
evaluate [push 7, push 4, binaryOp (-), binaryOp (+)] -- error
evaluate [push 7, push 4] -- error
evaluate [binaryOp' (-), push 7, push 4] where binaryOp' = binaryOp . flip
-- 3
----------------------------------------------------------------------
Here is the central equivalence for @case@ with guard qualifiers:
(*) case v of {p | qs_1 -> e_1
...
| qs_n -> e_n
where {decls};
_ -> e'}
= choice e' (do {p <- return v;
let {decls};
[e_1 | qs_1] ++ ... ++ [e_n | qs_n]})
It needs to be shown
1. that this equivalence is backward-compatible with equation (c) in
section 3.17.2 of the Haskell-1.4 report (Figure 3), i.e., that
case e' of
{y -> case v of {
p -> let { decls } in
if g_1 then e_1 ... else if g_n then e_n else y;
_ -> y }}
= choice e' (do {p <- return v;
let {decls};
[e_1 | g_1] ++ ... ++ [e_n | g_n]})
for boolean expressions g_1 ... g_n, and
2. that this equivalence is consistent with the borderline case of no
qualifiers, i.e., that
case v of {p -> e
where {decls};
_ -> e'}
= choice e' (do {p <- return v;
let {decls};
return e})
Note the use of @return e@ instead of @[e]@ because the latter syntax
does not work for non-list monads.
But before I go into that pain, I would like to get some feedback
whether you think it is worth the effort.
It should also be checked that (*) does not loop with the definitions of
the other language constructs used on the RHS. (At first sight I didn't
find a definition that uses pattern guards.)
If we do not use the enhanced language features, then the type checker
has no clue which @MonadChoice@ to use. In this case it should actually
not matter which one is used, and we can simply use @Maybe@ by default.
----------------------------------------------------------------------
Appendix
========
Note that for any @MonadChoice@ there is intuitively a natural coercion
to Maybe: If the monadic input value is @zero@, then the coercion is
@Nothing@. Otherwise the coercion is @Just x@, where @x@ is the value
returned by @choice@. Unfortunately, this coercion cannot be implemented
using @choice@. So we might think of the reverse approach where
@toMaybe@ is the class method and @choice@ is defined in terms of
@toMaybe@:
\begin{code}
class MonadToMaybe m where
toMaybe :: m a -> Maybe a
-- prime added to avoid conflict with earlier definition
choice' :: (MonadToMaybe m) => a -> m a -> a
choice' d m = case toMaybe m of
Nothing -> d
Just x -> x
instance MonadToMaybe Maybe where
toMaybe = id
instance MonadToMaybe [] where
toMaybe = listToMaybe
instance (InitialFinal a) => MonadToMaybe (STF a) where
toMaybe (STF t) = toMaybe [x | (x, s) <- t initial, final s]
\end{code}
According to these definitions a @MonadToMaybe@ is more powerful than a
@MonadChoice@. We therefore should check whether there is any reasonable
@MonadChoice@ that cannot be converted into a @MonadToMaybe@, before we
decide to use @MonadToMaybe@ instead of @MonadChoice@. Any ideas???
