Two-continuation `monads' and MonadMinus [Re: Parsers are monadic?]
When designing the full Kanren, we have experimented with two-continuation actions and various plumbing combinators (any, all, deterministic-all, etc). We eventually gave up on this after we realized that a simple interface suffices. Called MonadMinus, it is capable of defining LogicT monad with the true logical negation as well as interleaving and committed choice. Our ICFP05 paper describes MonadMinus monad (actually, the transformer) and LogicT as well as their two implementations. One of them uses success and failure continuations, and the other is based on delimited continuations. The latter offer an additional way to report `out-of-band' errors and continue parsing after the error has been `fixed'. http://okmij.org/ftp/Computation/monads.html#LogicT It is fair to say that whereas foldr/build and destroy/unfoldr fusion techniques work for Haskell lists, msplit/reflect in the LogicT paper is a fusion law for a general backtracking computation over arbitrary, perhaps even strict, base monad. That computation may look nothing like list; in fact, the LogicT paper gives an example with delimited continuations, with abort playing the role of nil and shift the role of cons.
oleg@pobox.com writes:
Called MonadMinus, it is capable of defining LogicT monad with the true logical negation as well as interleaving and committed choice. Our ICFP05 paper describes MonadMinus monad (actually, the transformer) and LogicT as well as their two implementations.
I just noticed that the Haskell wiki[1] claims that Data.Foldable
generalizes MonadMinus (aka MonadSplit).
[1] http://www.haskell.org/haskellwiki/New_monads
It's true that you can define msplit in terms of foldr, e.g.:
msplit :: (Foldable m, MonadPlus m) => m a -> m (Maybe (a, m a))
msplit a = foldr sk (return Nothing) a
where sk a m = return (Just (a, reflect m))
reflect :: MonadPlus m => m (Maybe (a, m a)) -> m a
reflect m = m >>= maybe mzero (\(a,m') -> return a `mplus` m')
But I can't help but feel that something is being lost.
I was initially skeptical about defining Foldable for the direct-style
LogicT transformer, but now I suspect that it is definable.
--
David Menendez
David Menendez writes:
oleg@pobox.com writes:
Called MonadMinus, it is capable of defining LogicT monad with the true logical negation as well as interleaving and committed choice. Our ICFP05 paper describes MonadMinus monad (actually, the transformer) and LogicT as well as their two implementations.
I just noticed that the Haskell wiki[1] claims that Data.Foldable generalizes MonadMinus (aka MonadSplit).
<snip>
But I can't help but feel that something is being lost.
Now that I think about it, you're losing the ability to work with monad
transformers.
That is, I don't think you can define a Foldable instance for
newtype NondetT m a
= NondetT (forall b. (a -> m b -> m b) -> m b -> m b)
--
David Menendez
I was initially skeptical about defining Foldable for the direct-style LogicT transformer, but now I suspect that it is definable.
Now that I think about it, you're losing the ability to work with monad transformers.
I think you're right. The particular point of msplit is that it is a monad transformer method and provides certain guarantees on the order and occurrences of _effects_. It seems the interface of Foldable, at brief glance, makes no assurances as to how foldr may behave. The implementation of foldr may decide to `look ahead' of the foldable data structure for optimization purposes and only then start invoking the folding function. That is sound so long as `looking ahead' does not entail any effect. The function `msplit' is designed to operate on a `data structure' where examining each element may be accompanied by an effect. It becomes important then not to look ahead and be careful not to re-do an effect if we need to re-examine some previously seen value. In short, msplit in LogicT does provide guarantees about the effect. The Foldable interface leaves this issue unspecified, or so it seems. So, they can't be considered equivalent. And speaking of non-determinism in general, it seem from experience FBackTrackT is a quite a better solver: it finds solutions where List and similar monads fail to find them; compared to the breadth-first search (which is too, complete), FBackTrackT takes far less resources. So, here too FBackTrackT finds solutions where breadth-first search just runs out of memory.
participants (2)
-
David Menendez -
oleg＠pobox.com