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
-- | 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)
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.
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.
-- | @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
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.
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.
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
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?
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.
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.
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.
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.
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.
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.