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.

3 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
2 Likes
#9

In the case where s = Bool this monad morphism witnesses the fact that the selection monad encodes a quantifier, like universal or existential quantification over some set. It seems that the joinSC function just evaluates the quantifier where the selection monad‘s join builds the quantifier on the fly.
In SC the selector and the quantifier may talk about different sets, though. You could for example search a singleton but quantify over a doubleton.

2 Likes
#10

Just thinking out loud, it looks optical, with runSelect as a getter and runCont as a setter. Maybe like an idempotent lens? runSC :: (a -> s) -> (s, a) reminds me of contrarepAdjunction where f ~ g.

#11

Isn’t your SC isomorphic to the selection monad J?

Martin Escardo and Paulo Oliva already described the monad morphism from the selection monad to the continuation monad:

(Overline function in Section 2)

so for

SC s a :: (a -> s) -> (s,a)
J s a :: (a -> s) -> a

we would have

j2sc e = \p ->  (p (e p), e p)
sc2j e = snd . e

I did not check if that actually is an isomorphism, but if I understand your SC correctly, that should be true.

Tom Schrijvers and I discovered something similar to this which you might want to check out:
https://kuleuven.limo.libis.be/discovery/fulldisplay?docid=lirias4158413&context=SearchWebhook&vid=32KUL_KUL:Lirias&lang=en&search_scope=lirias_profile&adaptor=SearchWebhook&tab=LIRIAS&query=any,contains,LIRIAS4158413&offset=0

1 Like
#12

I think this has been known in this thread, e.g. here. What is unclear is whether there are useful values of SC that are not of the form j2sc j (they definitely exist) and if so, whether these values can break the monad laws.
To this end, notice that even the traditional type J contains values that do not behave like a compact searchable set, despite the fact that all of J abides the monad laws.

intersects :: J Bool a -> (a -> Bool) -> Bool
intersects k p = p (k p)

For the value k to be set-like, we would expect intersects (\a -> x a || y a) == intersects k x || intersects k y and intersects k (const False) = False. (That is, intersects is a join-semilattice homomorphism.) But one can contrive examples that violate the former:

data Two = A | B deriving (Show,Eq)
instance Eq (Two -> Bool) where
    f == g = f A == g A && f B == g B
union :: (Two -> Bool) -> (Two -> Bool) -> Two -> Bool
union x y = \a -> x a || y a

a :: Two -> Bool
a = (==) A

b :: Two -> Bool
b = (==) B

strange :: J Bool Two
strange p = if p == b then A else B
-- intersects strange a == False
-- intersects strange b == False
-- intersects strange (union a b) == True
1 Like
#13

Aha, so the essence is that expressions like p (f p) do call p more often than needed and the G monad avoids it? Is the general monadic sequence and strength pair identical to the hand-written ones for G in the paper?

#14

There seems to be a straightforward projection from G to SC, hinting at a strong similarity:

type SC r a =           (a ->  r   ) -> (r,a)
type G  r a = forall b. (a -> (r,b)) -> (r,b)

g2sc :: G r a -> SC r a
g2sc g = \p -> let p' = \a -> (p a,a) in g p'

Maybe someone with a proof assistant can have a go at whether this is a monad morphism.

2 Likes
#15

Thank you for the suggestions! Like others already commented, I think SC s is a monad which is strictly larger than the selection monad J s. In other words, sc2j :: SC s ~> J s is not an isomorphism but an epimorphism with left inverse j2sc :: J s ~> SC s.

By quick-and-dirty calculation, the monad G s in your paper seems to have a natural isomorphism
(but not necessarily a monad isomorphism) with SC s.

G s a = ∀b. (a -> (s,b)) -> (s,b)
 ~ ∀b. ( (a -> (s,b)) -> s , (a -> (s,b)) -> b) )
 ~ ( (∀b. (a -> (s,b)) -> s) , (∀b. (a -> (s,b)) -> b) )
    -- No use of values of type b in the first component
 ~ ( (a -> s) -> s , K s a )
    -- (K s a ~ J s a) is in the Section 3.1 of the paper  
 ~ ( (a -> s) -> s, J s a)
 ~ SC s a

Probably the g2sc function in @olf’s comment is an isomorphism witnessing the above calculation.

Although I haven’t done anything to confirm it, if g2sc is a monad morphism, it implies that SC s is another, probably not very efficient, representation of your G s. The monad G s is (accidentally) a codensity monad Codensity ((,) s), which I understand to some extent.

Control.Monad.Codensity (hackage)

1 Like
#16

It looks like g2sc is a monad isomorphism!

This answers my initial question: SC s is a monad isomorphic to G s which is another name for Codensity ((,) s). It is used as an efficient implementation of the selection monad J s in (https://lirias.kuleuven.be/retrieve/759954), but only as a monad which can embed the selection monad. The usefulness of SC s which is not contained within the image of j2sc is still unclear.

#17

What a fascinating insight! Yet this makes me wonder: Codensity f is morally a more efficient version of Free f, isn’t it? (And if so, how is it related to Control.Monad.Free.Church?) This seems to imply that every selection function is isomorphic to the scored version of another selection function, or a pure value.
The original searchable sets of Escardo used the monoid s = Data.Monoid.Any whence (,) s is Applicative. How should we then understand Codensity-derived functions like

lift :: (s,a) -> G s a
lowerCodensity :: G s a -> (s,a)

Further I wondered how binary unions fit into this picture. There is a choice operation, not associative, but nevertheless:

instance Ord s => Alt ((,) s) where
   a@(sx,x) <!> b@(sy,y) = if sy > sx then b else a

I conjecture that this is what lets the Codensity version of selection functions compute binary unions.

1 Like
#18

I’ve been following this thread with great interest, as when it was first started I had just ended some experimentation with (a -> m r) -> m (a, r), which came up precisely because I wanted a more efficient Select, and my first attempt was to combine Select and Cont in this way. I then eventually discovered forall x. (a -> m (r, x)) -> m (r, x), because it directly encodes the fact that I basically just want to be able to call my continuation several times, observing part of the result but leaving the other part abstract. The resemblance to Codensity (WriterT r m) was a happy “coincidence,” because I absolutely did want r to be an instance of Monoid, because I was hoping to use it for probabilistic programming, where r would be unnormalized probabilities with the product monoid. I had some difficulty convincing myself that forall x. (a -> m (r, x)) -> m (r, x) was actually isomorphic to (a -> m r) -> m a (the fst and snd somehow tripped me up), and I also ended up deciding to try a totally different approach to my project, so I shelved these thoughts for later.

I don’t have the time to prove it right now, but I think this is associative. It’s the Future monoid/alt/alternative.

1 Like
#19

I also wondered about forall x. (a -> m (r, x)) -> m x, by the way. Maybe R is a way to figure that one out. No time to explore further now, but just figured I’d throw it out there either for my later self or for others.

#20

Hmm, you are right. Any nesting of <!> is equivalent to filtering for the maximum score and taking the first element of that non-empty list.

I don’t get the roles you have in mind for r and m. When m = WriterT (Product Prob) for some suitable real number type Prob, what is the scoring r doing? Can you not subsume the score into m?

I proved a theorem about lawfulness of certain monad constructions.
Consider a type T a isomorphic to

(a -> t) -> r

where t is the type of truth values and r is the result of the valuation, e.g. your type Prob. These monads can be embedded into the double dual (continuation) monad provided a notion of characteristic function t -> r. The prime example is when t = Bool and r is the closed real interval [0,1].
See Theorem 8 in section 8.9 in this document. The source is literate Haskell.