Nondeterminism, monadically

From HaskellWiki
Revision as of 07:25, 15 June 2022 by Atravers (talk | contribs) (Examples relabelled correctly, syntax corrected)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
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)