Sebastian Fischer wrote:
Consider the given Definitions of `CMaybe r a` with `fromCMaybe`, `mzero`, `mplus`, `orElse`, and additionally:
toCMaybe :: Maybe a -> CMaybe r a toCMaybe a = CMaybe (\k -> a >>= k)
getCMaybe :: CMaybe r a -> (a -> Maybe r) -> Maybe r getCMaybe (CMaybe a) = a
Much to my surprise, your example lead me to the following inequations:
a /= toCMaybe (fromCMaybe a)
because for ``a = return False `mplus` return True`` we have
getCMaybe a guard = Just () getCMaybe (toCMaybe (fromCMaybe a)) guard = Nothing
Also:
a /= mzero `orElse` a
because for the same `a` we have
getCMaybe a guard = Just () getCMaybe (mzero `orElse` a) guard = Nothing
Also:
a /= a `orElse` mzero
because for the same `a` we have
getCMaybe a guard = Just () getCMaybe (a `orElse` mzero) guard = Nothing
Pretty unfortunate. `mzero` is neither a left nor a right identity of `orElse`.
The reason is that in this implementation, orElse evaluates mplus too early x `orElse` (return False `mplus` return True) = x `orElse` return False and does not keep track of the fact that mplus does not decide for an alternative until the very end.
Is `mzero` an identity for `orElse` in your code or can we create a counter example like the one above? Can you add a distributive `mplus` to your code that would behave differently in the examples above?
In my code, mzero is indeed an identity for orElse as can be seen from the definition of the case eval kk (OrElse n m :>>= k) = case (eval kk' . view) n of ... -> ... MZeroR -> (eval kk . view) (m >>= k) where n evaluates to MZeroR . It shouldn't be difficult to add a distributive mplus ; it's definitely straightforward if we drop callCC . The observation is any action can be brought into one of the forms mzero return a `mplus` return b `mplus` ... which corresponds to the list type [a] . This, in turn, can be used to define orElse via pattern matching on the first argument. a `orElse` b = case a of { mzero -> b ; _ -> a } With the standard type definitions, the interpreter reads interpret :: Program Language a -> Maybe a interpret = listToMaybe . eval . view -- evaluate to a normal form eval :: ProgramView Language a -> [a] eval (Return a :>>= k) = [a] eval (MZero :>>= k) = [] eval (MPlus n m :>>= k) = (eval . view) (n >>= k) ++ (eval . view) (m >>= k) eval (OrElse n m :>>= k) = case (eval . view) n of [] -> (eval . view) (m >>= k) xs -> concatMap (eval . view . k) xs The call pattern of this interpreter shows that you can implement your type as newtype CMaybe a = CMaybe { forall b . (a -> [b]) -> [b] } but, as I said, this type is not good way of thinking about it in my opinion. Regards, Heinrich Apfelmus -- http://apfelmus.nfshost.com