haskell - 证明Maybe Applicative的组合律

Question

所以，我想手动证明 Maybe applicative 的组成定律是:

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

我用这些步骤来证明它:

u <*> (v <*> w)          [Left hand side of the law]
  = (Just f) <*> (v <*> w)  [Assume u ~ Just f]
  = fmap f (v <*> w)
  = fmap f (Just g <*> w)   [Assume v ~ Just g]
  = fmap f (fmap g w)
  = fmap (f . g) w

pure (.) <*> u <*> v <*> w  [Right hand side of the law]
  = Just (.) <*> u <*> v <*> w
  = fmap (.) u <*> v <*> w
  = fmap (.) (Just f) <*> v <*> w  [Replacing u with Just f]
  = Just (f .) <*> v <*> w
  = Just (f .) <*> Just g <*> w    [Replacing v with Just g]
  = fmap (f .) (Just g) <*> w
  = Just (f . g) <*> w
  = fmap (f . g) w

这样证明正确吗？我真正关心的是我假设 u和 v对于嵌入在 Just 中的一些功能数据构造函数继续我的证明。这可以接受吗？有没有更好的方法来证明这一点？

Answer 1

应用仿函数表达式只是某些仿函数上下文中的函数应用程序。因此:

pure f <*> pure a <*> pure b <*> pure c

-- is the same as:

pure (f a b c)

我们想证明:

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

考虑:

u = pure f
v = pure g
w = pure x

因此，左边是:

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

pure (.) <*> pure f <*> pure g <*> pure x

pure ((.) f g x)

pure ((f . g) x)

pure (f (g x))

pure f <*> pure (g x)

pure f <*> (pure g <*> pure x)

u <*> (v <*> w)

对于 Maybe我们知道 pure = Just .因此，如果 u , v和 w是 Just值然后我们知道组合定律成立。

但是，如果其中任何一个是 Nothing 怎么办？ ?我们知道:

Nothing <*> _ = Nothing
_ <*> Nothing = Nothing

因此，如果其中任何一个是 Nothing那么整个表达式变为 Nothing (如果第一个参数是 undefined 则在第二种情况下除外)并且因为 Nothing == Nothing法律仍然有效。

最后， undefined 呢？ (又名底部)值？我们知道:

(Just f) <*> (Just x) = Just (f x)

因此，以下表达式将使程序停止:

(Just f) <*> undefined
undefined <*> (Just x)
undefined <*> Nothing

然而，下面的表达式将导致 Nothing :

Nothing <*> undefined

在这两种情况下，组合法仍然成立。