Nondeterminism, monadically
Jump to navigation
Jump to search
The printable version is no longer supported and may have rendering errors. Please update your browser bookmarks and please use the default browser print function instead.
From figure 8 (on page 8 of 12) in Deriving Backtracking Monad Transformers by Ralf Hinze, in more-contemporary syntax:
newtype NondetT m a
= NondetT { mkNondetT :: (forall b. (a -> m b -> m b) -> m b -> m b) }
runNondetT :: (Monad m) => NondetT m a -> m a
runNondetT m = mkNondetT m (\a f -> return a) (fail "false")
instance (Monad m) => Monad (NondetT m) where
return a = NondetT (\c -> c a)
m >>= k = NondetT (\c -> mkNondetT m (\a -> mkNondetT (k a) c))
instance (Monad m) => MonadPlus (NondetT m) where
mzero = NondetT (\c -> id)
m1 `mplus` m2 = NondetT (\c -> mkNondetT m1 c . mkNondetT m2 c)
instance MonadTrans NondetT where
lift m = NondetT (\c f -> m >>= \a -> c a f)
As a regular monadic type:
newtype Nondet a
= Nondet { mkNondet :: (forall b. (a -> b -> b) -> b -> b) }
runNondet :: (Monad m) => Nondet a -> m a
runNondet m = mkNondet m (\a f -> return a) (fail "false")
instance Monad Nondet where
return a = Nondet (\c -> c a)
m >>= k = Nondet (\c -> mkNondet m (\a -> mkNondet (k a) c))
instance MonadPlus Nondet where
mzero = Nondet (\c -> id)
m1 `mplus` m2 = Nondet (\c -> mkNondet m1 c . mkNondet m2 c)