Can the continuation monad transformer be given an Alternative instance with some and many?
Asked Answered
K

1

14

We can define the continuation monad transformer as

data Cont r m a = Cont {run :: (a -> m r) -> m r}

We can give Cont r m an Alternative instance if m is a member of Alternative via

empty = Cont $ \f -> empty
ca <|> cb = Cont $ \f -> run ca f <|> run cb f

And then allow some and many to take on their default methods. My question is, can we define some and many in terms of m's some and many, instead of the default definitions? The apparently obvious options

some ca = Cont $ \f -> some $ run ca f
many ca = Cont $ \f -> many $ run ca f

obviously do not work (they do not even type check). Is there some other way to use them (if we need m to also be a monad, that's fine)?

For reference, some and many must be the least solution to the equations:

  • some v = (:) <$> v <*> many v
  • many v = some v <|> pure []

Assuming that some :: m a -> m [a] and many :: m a -> [a] satisfy this law, so should some :: Cont r m a -> Cont r m [a] and many :: Cont r m a -> Cont r m [a].

Kaleb answered 28/11, 2017 at 5:33 Comment(0)
C
4

No.

There exists no arrow from

(forall a. f a -> f [a]) ->
(forall r. ((a -> f r) -> f r)) -> (([a] -> f r) -> f r)`

that makes use of its argument in an interesting way.

The only place forall a. f a -> f [a] can be applied is to an f r. These are the results of (a -> f r) -> f r, like in your "obvious options", and ([a] -> f r). This leaves a result of the type f [r]. The only thing that can be done with a forall r. Alternative f => f [r] to produce an f r is index the f [r] with some partial function forall r. [r] -> r from a natural number to some other no-larger natural number.

Carnage answered 28/11, 2017 at 21:17 Comment(5)
If r had some additional structure, however, perhaps something could be done. For example maybe we could fmap fold the f [r], and with suitable coherence laws that could be equivalent.Condescend
I would beg to differ. some ca = Cont $ \fla -> run ca $ \a -> (some $ pure a) >>= fla is sort of interesting. The question is whether this is a valid some instance.Kaleb
You can't get the [a] out of an f [a] like some $ pure a with only an Alternative f constraint. You need either Monad f or Traversable f to do anything with it.Carnage
@Condescend Yes, that's why I was very explicit with the forall rs.Carnage
I mentioned that I was fine with f being a Monad. This post is useful though, showing that Monad is in fact required to even get it to type-check.Kaleb

© 2022 - 2024 — McMap. All rights reserved.