Nondeterminism, monadically

From HaskellWiki
Revision as of 06:24, 9 March 2021 by Atravers (talk | contribs) (Initial content)
(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 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)

As a regular monadic type:

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)