Nondeterminism, monadically
Jump to navigation
Jump to search
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)