是的，看起来这是一个合法的Applicative。奇怪！

正如@JosephSible所指出的，你可以从定义中立即读出恒等、同态和交换定律。唯一棘手的是合成定律。

pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

有八个箱子要检查，所以系好安全带。

• 一个箱子有三个Return：pure (.) <*> Return f <*> Return g <*> Return z
• 从(.)的结合性可以得出。
• 三种情况下有一个Free：
• pure (.) <*> Free u <*> Return g <*> Return z
• 从Free u <*> (Return g <*> Return z)向后计算得到fmap (\f -> f (g z)) (Free u)，所以这是由函子定律得出的。

pure (.) <*> Return f <*> Free v <*> Return z
fmap ($z) $ fmap f (Free v)
fmap (\g -> f (g z)) (Free v)                  -- functor law
fmap (f . ($z)) (Free v)
fmap f (fmap ($z) (Free v))                    -- functor law
Return f <$> (Free v <*> Return z)             -- RHS of `<*>` (first and second cases)
QED

• pure (.) <*> Return f <*> Return g <*> Free w
• 立即简化为fmap (f . g) (Free w)，所以从函子定律得出。
• 三种情况下有一种Return：

pure (.) <*> Return f <*> Free v <*> Free w
Free $ fmap (<*>) (fmap (fmap (f.)) v) <*> w
Free $ fmap (\y z -> fmap (f.) y <*> z) v <*> w                  -- functor law
Free $ fmap (\y z -> fmap (.) <*> Return f <*> y <*> z) v <*> w  -- definition of fmap, twice
Free $ fmap (\y z -> Return f <*> (y <*> z)) v <*> w             -- composition
Free $ fmap (\y z -> fmap f (y <*> z)) v <*> w                   -- RHS of fmap, definition of liftA2
Free $ fmap (fmap f) $ fmap (<*>) v <*> w                        -- functor law, eta reduce
fmap f $ Free $ liftA2 (<*>) v w                                 -- RHS of fmap
Return f <*> Free v <*> Free w                                   -- RHS of <*>
QED.

pure (.) <*> Free u <*> Return g <*> Free w
Free ((fmap (fmap ($g))) (fmap (fmap (.)) u)) <*> Free w
Free (fmap (fmap (\f -> f . g) u)) <*> Free w                    -- functor law, twice
Free $ fmap (<*>) (fmap (fmap (\f -> f . g)) u) <*> w
Free $ fmap (\x z -> fmap (\f -> f . g) x <*> z) u <*> w         -- functor law
Free $ fmap (\x z -> pure (.) <*> x <*> Return g <*> z) u <*> w
Free $ fmap (\x z -> x <*> (Return g <*> z)) u <*> w             -- composition
Free $ fmap (<*>) u <*> fmap (Return g <*>) w                    -- https://gist.github.com/benjamin-hodgson/5b36259986055d32adea56d0a7fa688f
Free u <*> fmap g w                                              -- RHS of <*> and fmap
Free u <*> (Return g <*> w)
QED.

pure (.) <*> Free u <*> Free v <*> Return z
Free (fmap (<*>) (fmap (fmap (.)) u) <*> v) <*> Return z
Free (fmap (\x y -> fmap (.) x <*> y) u <*> v) <*> Return z        -- functor law
Free $ fmap (fmap ($z)) (fmap (\x y -> fmap (.) x <*> y) u <*> v)
Free $ liftA2 (\x y -> (fmap ($z)) (fmap (.) x <*> y)) u v         -- see Lemma, with f = fmap ($z) and g x y = fmap (.) x <*> y
Free $ liftA2 (\x y -> fmap (.) x <*> y <*> Return z) u v          -- interchange
Free $ liftA2 (\x y -> x <*> (y <*> Return z)) u v                 -- composition
Free $ liftA2 (\f g -> f <*> fmap ($z) g) u v                      -- interchange
Free $ fmap (<*>) u <*> (fmap (fmap ($z)) v)                       -- https://gist.github.com/benjamin-hodgson/5b36259986055d32adea56d0a7fa688f
Free u <*> Free (fmap (fmap ($z)) v)
Free u <*> (Free v <*> Return z)
QED.

• 三个Free：pure (.) <*> Free u <*> Free v <*> Free w
• 本例只练习了<*>的Free/Free的情况，其右侧与Compose的<*>的右侧相同，所以本例是从Compose的示例的正确性出发得出的。

对于pure (.) <*> Free u <*> Free v <*> Return z的情况，我使用了一个引理：

引理：fmap f (fmap g u <*> v) = liftA2 (\x y -> f (g x y)) u v。

fmap f (fmap g u <*> v)
pure (.) <*> pure f <*> fmap g u <*> v  -- composition
fmap (f .) (fmap g u) <*> v             -- homomorphism
fmap ((f .) . g) u <*> v                -- functor law
liftA2 (\x y -> f (g x y)) u v          -- eta expand
QED.

在归纳假设下，我使用函子和应用定律。
这证明起来非常有趣！我希望看到Coq或Agda的正式证明（尽管我怀疑终结/积极性检查器可能会把它搞砸）。

For the sake of completeness, I will use this answer to expand on my comment above:
Though I didn't actually write down the proof, I believe the mixed-Free-and-Return cases of the composition law must hold due to parametricity. I also suspect that should be easier to show using the monoidal presentation .
The monoidal presentation of the Applicative instance here is:

unit = Return ()

Return x *&* v = (x,) <$> v
u *&* Return y = (,y) <$> u
-- I will also piggyback on the `Compose` applicative, as suggested above.
Free u *&* Free v = Free (getCompose (Compose u *&* Compose v))

Under the monoidal presentation, the composition/associativity law is:

(u *&* v) *&* w ~ u *&* (v *&* w)

Now let's consider one of its mixed cases; say, the Free - Return - Free one:

(Free fu *&* Return y) *&* Free fw ~ Free fu *&* (Return y *&* Free fw)

(Free fu *&* Return y) *&* Free fw -- LHS
((,y) <$> Free fu) *&* Free fw

Free fu *&* (Return y *&* Free fw) -- RHS
Free fu *&* ((y,) <$> Free fw)

Let's have a closer look at this left-hand side. (,y) <$> Free fu applies (,y) :: a -> (a, b) to the a values found in Free fu :: FreeMonad f a . Parametricity (or, more specifically, the free theorem for (*&*) ) means that it doesn't matter if we do that before or after using (*&*) . That means the left-hand side amounts to:

first (,y) <$> (Free fu *&* Free fw)

Analogously, the right-hand side becomes:

second (y,) <$> (Free fu *&* Free fw)

Since first (,y) :: (a, c) -> ((a, b), c) and second (y,) :: (a, c) -> (a, (b, c)) are the same up to reassociation of pairs, we have:

first (,y) <$> (Free fu *&* Free fw) ~ second (y,) <$> (Free fu *&* Free fw)
-- LHS ~ RHS

The other mixed cases can be dealt with analogously. For the rest of the proof, see Benjamin Hodgson's answer .

由Applicative的定义可知：
如果f也是Monad，则应满足

• x一m三n一x = x一m四n一x
• (<*>) = ap
• (*>) = (>>)

因此，这种实现将违反适用法律，即它 * 必须 * 与Monad示例一致。
也就是说，没有理由不能为FreeMonad创建一个newtype Package 器，它没有monad示例，但有上面的applicative示例

newtype Zip f a = Zip { runZip :: FreeMonad f a }
  deriving Functor

instance Applicative f => Applicative (Zip f) where -- ...