{-# LANGUAGE ExistentialQuantification #-} -- A taste for extensible effects and masking -- A warm-up with a more complex example: non-determinism module Nondet where import Control.Monad.Cont -- We start with the Cont r monad. It is certainly a monad, for -- all r. We don't need to prove it; It has been proven already. -- The non-determinism effect -- choice lst non-deterministically chooses one value from the lst -- choice [] thus corresponds to failure data Choose w = forall a. Choose [a] (a -> w) newtype Mu f = In{unmu:: f (Mu f)} -- We carry the effect in types, including the absence of effect! -- The result of the computation: a value or an effect (request) data VE a s self = Val a | E (s self) -- Now, the answer-type is recursive choice :: [a] -> Cont (Mu (VE w Choose)) a choice lst = Cont (\k -> In . E \$ (Choose lst k)) -- MonadPlus-like operators are expressible via choice mzero' :: Cont (Mu (VE w Choose)) a mzero' = choice [] -- The (inferred) type of mplus' shows the effect mplus' :: Cont (Mu (VE w Choose)) b -> Cont (Mu (VE w Choose)) b -> Cont (Mu (VE w Choose)) b mplus' m1 m2 = choice [m1,m2] >>= id -- The interpreter makeChoice :: Cont (Mu (VE a Choose)) a -> Cont w [a] makeChoice (Cont m) = loop (m (In . Val)) where loop (In (Val x)) = return [x] loop (In (E (Choose [] _))) = return [] loop (In (E (Choose [x] k))) = loop (k x) loop (In (E (Choose lst k))) = fmap concat \$ mapM (loop . k) lst -- Now, run no longer has any `error' -- (compare with run in TermAlgebra.hs) run :: Cont a a -> a run (Cont m) = m id -- Examples add :: Cont w Int -> Cont w Int -> Cont w Int add = liftM2 (+) -- The type is inferred ex1 :: Cont w Int ex1 = return 1 `add` return 2 ex1r = run ex1 -- 3 -- The type is inferred ex2 :: Cont (Mu (VE w Choose)) Int ex2 = return 1 `add` choice [1,2] -- The following won't type: unhandled effect! -- ex2r = run ex2 {- Couldn't match expected type `Mu (VE w0 Choose)' with actual type `Int' Expected type: Cont (Mu (VE w0 Choose)) (Mu (VE w0 Choose)) Actual type: Cont (Mu (VE w0 Choose)) Int -} -- The inferred type shows that ex21 is now pure -- ex21 :: Cont w [Int] ex21 = makeChoice ex2 ex21r = run ex21 -- [2,3] -- Pythagorean triples ex3 :: Cont (Mu (VE w Choose)) (Int, Int, Int) ex3 = do x <- choice [1..10] y <- choice [1..10] z <- choice [1..10] if x*x + y*y == z*z then return (x,y,z) else mzero' ex3r = run . makeChoice \$ ex3 -- [(3,4,5),(4,3,5),(6,8,10),(8,6,10)]