可能适用的证明成分法

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

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

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

在任何一种情况下,构成法仍然有效.