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].

duplode
  • 33,731
  • 7
  • 79
  • 150
PyRulez
  • 10,513
  • 10
  • 42
  • 87

1 Answers1

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.

Cirdec
  • 24,019
  • 2
  • 50
  • 100
  • 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. – luqui Nov 29 '17 at 21:49
  • 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. – PyRulez Nov 29 '17 at 22:58
  • 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. – Cirdec Nov 30 '17 at 02:34
  • @luqui Yes, that's why I was very explicit with the `forall r`s. – Cirdec Nov 30 '17 at 02:38
  • 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. – PyRulez Nov 30 '17 at 02:55