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, search

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)