-
Notifications
You must be signed in to change notification settings - Fork 21
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Composition w/ Selective #12
Comments
@awhtayler Yes, that's an interesting question which I've been thinking about for a while. We do have the instance you mention: selective/src/Control/Selective.hs Lines 392 to 393 in edd7dfc
In a way, you can say that this composition uses Curiously, instance (Alternative f, Applicative g) => Alternative (Compose f g) where
Maybe, but I'd like to make this intuition a bit more precise. Could you elaborate a bit further?
As we discuss in the paper, there are some alternative definitions of selective functors, which include methods like |
Here is an example showing why composing selective functors is tricky. Consider select :: Maybe (IO (Either a b)) -> Maybe (IO (a -> b)) -> Maybe (IO b)
select Nothing _ = Nothing
select (Just x) (Just y) = Just (select x y)
select (Just x) Nothing = Nothing -- Can't use Just: we don't have the function a -> b! In other words, we have to be |
If your inner functor is also instance (Applicative g, Traversable g, Selective g) => Selective (Compose Maybe g) where
select (Compose Nothing) (Compose Nothing) = Compose Nothing
select (Compose Nothing) (Compose (Just g)) = Compose Nothing
select (Compose (Just g)) (Compose Nothing) = Compose $ either (const Nothing) Just $ sequenceA g
select (Compose (Just g)) (Compose (Just g')) = Compose $ Just $ select g g' The key is that we can I didn't check the laws though. There is a generalisation of this idea: instance (Traversable g, Applicative g, Selective f) => Selective (Compose f g) where
select (Compose eab) (Compose fab) = Compose $ select (sequenceA <$> eab) (sequenceA <$> fab) The first Again I didn't check the laws, but we could start that with some property tests, and then look for a proof. |
A lot of functors are traversable. Most from Any functor of the sort |
Let's look at some laws. Identityx <*? pure id
-- definition of my instance and `Applicative Compose`
= Compose $ select (sequenceA <$> getCompose x) (sequenceA <$> pure (pure id))
-- `Applicative` law
= Compose $ select (sequenceA <$> getCompose x) (pure sequenceA <*> pure (pure id))
-- `Applicative` law
= Compose $ select (sequenceA <$> getCompose x) (pure (sequenceA id))
-- `Functor` and `Traversable` law
= Compose $ select (sequenceA <$> getCompose x) (pure id)
-- `Selective` law
= Compose $ either id id <$> (sequenceA <$> getCompose x)
-- Definition of `Compose`
= either id id <$> x Distributivitypure x <*? (y *> z)
-- definition of instance and `Applicative Compose`
= Compose $ select (sequenceA <$> pure (pure x)) (getCompose (y *> z))
-- `Applicative` law
= Compose $ select (pure sequenceA <*> pure (pure x)) (getCompose (y *> z))
-- `Applicative` law
= Compose $ select (pure (sequenceA (pure x))) (getCompose (y *> z))
-- `Compose` & `Applicative` lemma
= Compose $ select (pure (sequenceA (pure x))) (getCompose y *> getCompose z)
-- `Selective` law
= Compose $ select (pure (sequenceA (pure x))) (getCompose y) *> (pure (sequenceA (pure x))) (getCompose z)
-- Previous steps backwards
= (pure x <*? y) *> (pure x <*? z) AssociativityThat sounds hard. |
NoteBy the way, the second instance (Traversable g, Applicative g, Selective f) => Selective (Compose f g) where
select (Compose eab) (Compose fab) = Compose $ select (sequenceA <$> eab) (strength <$> fab)
strength :: Functor g => g (a -> b) -> a -> g b
strength g a = fmap ($ a) g This is because in Haskell, every functor is strong. But to get something of type |
AssociativityTo prove: x <*? (y <*? z) = (f <$> x) <*? (g <$> y) <*? (h <$> z)
where
f :: Either a b -> Either a (Either e b)
f x = Right <$> x
g :: Either c (a -> b) -> a -> Either (c, a) b
g y = \a -> bimap (,a) ($a) y
h :: (c -> a -> b) -> (c, a) -> b
h z = uncurry z ((f <$> x) <*? (g <$> y)) <*? (h <$> z)
-- Definition
= Compose $ (sequenceA <$> getCompose (f <$> x)) <*? (sequenceA <$> getCompose (g <$> y)) <*? (sequenceA <$> getCompose (h <$> z))
-- Definition of `<$>` in `Compose`
= Compose $ (sequenceA <$> (fmap f <$> getCompose x)) <*? (sequenceA <$> (fmap g <$> getCompose y)) <*? (sequenceA <$> (fmap h <$> getCompose z))
-- `<$>` law
= Compose $ (sequenceA . fmap f <$> getCompose x) <*? (sequenceA . fmap g <$> getCompose y) <*? (sequenceA . fmap h <$> getCompose z)
-- Naturality of `Traversable` (https://hackage.haskell.org/package/base-4.12.0.0/docs/Data-Traversable.html#t:Traversable)
-- Since `f`, `g` and `h` are applicative transformations
= Compose $ (f . sequenceA <$> getCompose x) <*? (g . sequenceA <$> getCompose y) <*? (h . sequenceA <$> getCompose z)
-- `<$>` law
= Compose $ (f <$> sequenceA <$> getCompose x) <*? (g <$> sequenceA <$> getCompose y) <*? (h <$> sequenceA <$> getCompose z)
-- Associativity of underlying `Selective`
= Compose $ (sequenceA <$> getCompose x) <*? ((sequenceA <$> getCompose y) <*? (sequenceA <$> getCompose z))
-- Definition of instance
= x <*? (y <*? z) Bottom lineSo I guess we have a By the way, the Lemmata:
|
The two definitions are equivalent since for any fmap f = runIdentity . sequenceA . fmap (Identity . f) And thus strength g a
= fmap ($ a) g
= (runIdentity . sequenceA . fmap (Identity . ($ a))) g
-- Naturality of `sequenceA`.
-- Now this is just a silly way of currying:
= (($ a) . sequenceA) g
-- Let's eta-expand to see this
= (\g' -> ($ a) $ sequenceA g') g
= (\g' -> sequenceA g' a) g
= sequenceA g a So for proofs and reasoning we may still assume that the instance is defined symmetrically with |
@turion Cool, thanks for working out all the proofs! I did know that one can get the composition to type check with One problem with using this definition is that it looks somewhat arbitrary (just like the one used in the library at the moment). Let's look at the two instances:
Why would one pick one over the other? Surely, neither of them is more general. Intuitively, we want the composition of two selective functors to "respect" their individual selectivity, but neither of these instances can do that since they use only one I suspect we are really looking for |
Yes, that's true. There can be situations where only one applies, or maybe even both. For the case that both apply, we'd need two different newtypes. It would be interesting to see whether the two variants agree in such a case, or what extra compatibility between
Yes, that's strange. I see this as both a strength and a weakness. The strength in this is that we can sometimes combine a
I agree that this would be the optimum. But I'm not sure it's achievable. In some sense you already have this for the first definition, since For the second definition, it is the other way around. You probably already know that newtype TraverseSelective f a = TraverseSelective { getTraverseSelective :: f a }
deriving (Functor, Applicative)
instance (Applicative f, Traversable f) => Selective (TraverseSelective f) where
select eab fab = TraverseSelective $ either (strength $ getTraverseSelective fab) id $ sequenceA $ getTraverseSelective eab In fact, the But there is some inherent choice in this. I'm not sure there is a way to have a more general formulation that encompasses both. In fact, I'd intuitively think that this can't be. |
Actually, I didn't know about it, thanks for sharing! Now the two selectA :: Applicative f => f (Either a b) -> f (a -> b) -> f b
selectA x y = (\e f -> either f id e) <$> x <*> y
selectT :: (Applicative f, Traversable f) => f (Either a b) -> f (a -> b) -> f b
selectT x y = case sequenceA x of
Left a -> ($a) <$> y
Right fb -> fb
λ> selectA (Const "x") (Const "y")
Const "xy"
λ> selectT (Const "x") (Const "y")
Const "x"
Yes, this makes a lot of sense. |
CommentOne would usually call functorial strength this function: strength :: Functor g => (a, g b) -> g (a, b)
strength (a, gb) = (a, ) <$> gb With currying and function application we arrive at the other function But there is a co-concept to that, by replacing products with sums and reversing the direction of the arrows: class Functor f => Costrong f where
costrength :: f (Either a b) -> Either a (f b) This is not automatically satisfied for Haskell functors. But it exists for The punch line is that Relation to your observationSo since Composition of extra structuresBut it's unclear how, or whether two general
Depending on what the functors are, there may be other ways to give
I'm wondering how the choice of distributive law can change the Selective morphismsDefinition: Let Question: Is there a If yes, then I think this is "The Right" composed structure. It necessarily has to incorporate both But right now my impression is that there is no such structure canonically for all selective functors. Our two cases seem not to give rise to selective morphisms because they don't use both selective structures. (And my variant even needs an extra typeclass.) Another line of research might be looking for a "distributive law", maybe something like |
Aha, Note that there seem to be yet another implementation of class Costrong2 f where
costrength2 :: f (Either a b) -> Either (f a) b
selectC2 :: (Applicative f, Costrong2 f) => f (Either a b) -> f (a -> b) -> f b
selectC2 x y = case costrength2 x of
Left fa -> fa <**> y
Right b -> pure b Not sure it makes sense but symmetry would suggest that it should. I like how you frame the composition problem in terms of "selective morphisms"! |
Good point about your It's probably clear, but let me just note that every functor that has For functorial strength I believe no other laws than naturality are required, so translated to In the proof for |
Sure, I can see that.
On the one hand, this makes the picture less clear. On the other hand, it's probably not surprising that one can come up with a lot of different ways to construct selective functors. There are many functors and many ways to make decisions based on different flavours of "inspectability", including oddities like "if the third element of the traversable functor is |
Yes, there is suddenly a big design space. The difference between So, yes, I agree, there doesn't seem to be one clear way to compose them, but lots of clever and also silly ways. The right question still is "what's the most general extra structure to give a |
I was wondering if it mightn't be instructive to somewhere discuss what happens when you try to compose with Selective functors.
It seemed to me that you can only ever recover the selectivity of the inner functor, ie.
The outer functor
f
is executed unconditionally, but selective behaviour of the inner functorg
is preserved.I believe (?) that eg.
Selective f, Selective g
doesn't permit conditional execution off
inSelective (Compose f g)
, likewiseSelective f, Applicative g
.Does this perhaps help illustrate the way in which the potential effects are statically constrained - in particular the selective execution can't depend on the results of other arbitrary functors which with they are composed?
Also, is there any scope for exploring a stronger notion of "compositional selectivity"? Where we would be allowed to say if
f
,g
do not execute the unchosen branch, then their composition won't do either?The text was updated successfully, but these errors were encountered: