A new kind of Continuation-like Monad?

Learn
#1

Recently (I think) I found the following Monad. Is this known somewhere? Is there any usage of it for programming? (Or I’m totally wrong, and it’s not a lawful Monad at all?)

-- | It /looks/ like it is the product monad of 'Control.Monad.Trans.Select.Select' and
--   'Control.Monad.Trans.Cont.Cont' ...
--   but it isn't! The two components are not independent.
data SC s a = SC {
    runSelect :: (a -> s) -> a,
    runCont :: (a -> s) -> s
  }
  deriving Functor

instance Applicative (SC s) where
  pure = pureSC
  (<*>) = ap
instance Monad (SC s) where
  ma >>= k = joinSC (fmap k ma)

pureSC :: a -> SC s a
pureSC x = SC { runSelect = const x, runCont = ($ x) }

joinSC :: SC s (SC s a) -> SC s a
joinSC mmx = SC { runSelect = selPart, runCont = contPart }
  where
    contPart = \f -> runCont mmx (\mx -> runCont mx f)
    selPart = \f -> runSelect (runSelect mmx (\mx -> runCont mx f)) f

Compare it with Selection monad and Continuation monad:

-- | Continuation monad
newtype C s a = C { runC :: (a -> s) -> s }
  deriving Functor

pureC :: a -> C s a
pureC x = C ($ x)

joinC :: C s (C s a) -> C s a
joinC mmx = C $ \f -> runC mmx (\mx -> runC mx f)

-- | Selection monad
newtype S s a = S { runS :: (a -> s) -> a }
  deriving Functor

pureS :: a -> S s a
pureS x = S $ const x

joinS :: S s (S s a) -> S s a
joinS mmx = S $ \f -> runS (runS mmx (\mx -> f (runS mx f))) f

Note that the Cont part of the new monad SC s is exactly the continuation monad C s, but the Select part is not just a translation of S s. joinSC of the Select part depends on the Cont part.

The following links are the code (and how I’ve derived this Monad)

4 Likes
#2

I checked the laws by manual rewriting. They seem to hold unless I’ve made a substitution mistake in the process.

2 Likes
#3

It looks like Select where the computation returns both the “selected” value a and the “score” s. Indeed, this is a monad morphism:

morph :: S s a -> SC s a
morph (S f) = SC f (\k -> k (f k))

(Coq proof of the monad morphism laws)

One way SC could be more expressive than S is by having computations not expressible as morph f for some f :: S s a. It’s not difficult to come up with artificial examples, but perhaps there are more natural examples to adapt from the paper(s) on the selection monad.

3 Likes
#4

Could the monad be defined as

data SC s a = SC {
    runSC :: (a -> s) -> (s, a)
  }

?

2 Likes
#5

Yes! In fact, I have transformed to SC from that type to emphasize it contains the continuation monad C as a component of the direct product.

#6

Thank you for the checking. I’ve only done checking of Monad laws on few concrete values (like QuickCheck but makeshift, deterministic test)

#7

Thank you for the comment. I didn’t noticed there’s a monad morphism S s ~> SC s in addition to projection C . runCont :: SC s ~> C s which happens to be a monad morphism too.

Seeking examples from the papers about selection monads sounds good! If I recall correctly there should be something about logic programming -esque applications.

#8

I think it is better to write down how I’ve noticed this is a Monad, which is buried in the multiple places I linked in the first post.

First, I noticed the following R w is a Monad for every Comonad w while experimenting with
adjunctions between categories Set and Poly (PDF link) for
my recent functor-monad library.

-- | @R w@ is 'Monad' for every 'Comonad' @w@
newtype R w a = R { runR :: forall r. (a -> w r) -> r }
  deriving Functor

instance Comonad w => Applicative (R w) where
  pure x = R $ \k -> extract (k x)
  (<*>) = ap

instance Comonad w => Monad (R w) where
  rw >>= k = R $ \cont -> runR rw (\x -> runR (k x) (duplicate . cont))

In diagram, its monad operations are written like below:

pure =
    a
      ↓ iso
    ∀r. (a -> r) -> r
      ↓ contravariantly map (extract :: ∀x. w x -> x)
    ∀r. (a -> w r) -> r
      ||
    R w a

join =
    R w (R w a)
      ||
    ∀r. (R w a -> w r) -> r
      ↓ covariantly map
      ↓   run :: R w a -> (a -> w (w r)) -> w r
      ↓   run = runR ma @(w r)
    ∀r. (((a -> w (w r)) -> w r) -> w r) -> r
      ||
    ∀r. Cont (w r) (a -> w (w r)) -> r
      ↓ contravariantly map
      ↓     pure :: (a -> w (w r)) -> Cont (w r) (a -> w (w r))
    ∀r. (a -> w (w r)) -> r
      ↓ contravariantly map (duplicate :: ∀x. w x -> w (w x))
    ∀r. (a -> w r) -> r
      ||
    R w a

I tried to understand this monad by calculating examples of R w by substituting w with concrete comonads. For example, R (Traced m) was isomorphic to Writer m monad. The monad SC s is R w when w is the Store s comonad.

R (Store s) a
〜 ∀r. (a -> (s -> r, s)) -> r
〜 ∀r. (a -> s -> r, a -> s) -> r
〜 ∀r. (a -> s -> r) -> (a -> s) -> r
〜 (a -> s) -> ∀r. (a -> s -> r) -> r
〜 (a -> s) -> (a, s)
〜 (a -> s -> a, a -> s -> s)
〜 SC s a
1 Like