Under "Why do Static Arrows generalise Arrows?" post, we often spoke of Applicative running side-effects before the application of the function-in-the-functor to the value-in-the-functor.
Also, danidiaz used this fact to show that Arrow is not equivalent to Applicative in this answer under "Arrows are exactly equivalent to applicative functors?" question.
How is this property formalised?
For Applicative, that can be justified through parametricity. Consider...
(&*&) :: Applicative f => f a -> f b -> f (a, b)
... which is the counterpart to (<*>) in the monoidal presentation of Applicative. Restricted to functions, the free theorem for (&*&) is:
fmap g u &*& fmap h v = fmap (bimap g h) (u &*& v)
(The free theorem is actually more general than that, as it allows for relations that aren't functions to play the roles of g and h.)
The free theorem means that if we change the values-in-the-functor of u or v, the result of (&*&) will only be affected by its corresponding values-in-the-functor being changed in the same manner. In other words, as far as (&*&) is concerned the values-in-the-functor have no influence over the applicative effects, which is what you intended to establish.
