haskell - 观察同构，然后证明它们是 Monad

Question

这个问题与这个answer有关.

有一个类型名为 Promise :

data Promise f a =  PendingPromise f | ResolvedPromise a | BrokenPromise deriving (Show)

据称:

Promise f a ≅ Maybe (Either f a)

现在我无法理解上面的表达。他们怎么样
等价和同构(从那你怎么能断定它
是一个单子(monad))？

Answer 1

两种类型A和 B如果有两个函数 a2b :: A -> B 是同构的和 b2a :: B -> A这样a2b . b2a ≡ id和 b2a . a2b ≡ id .在这个例子中，这很容易证明:两个函数的子句基本相同，只有 = 的边。转身，例如

promise2Trafo (PendingPromise f) = ErrorT . Just $ Left f
trafo2Promise (ErrorT (Just (Left f))) = PendingPromise f

因此，以任一顺序组合函数都会为您提供标识函数。同构的关键在于 a2b x ≡ a2b y仅当且仅当 x ≡ y 成立.

现在，这对证明类型类定律有何帮助？再次从示例中提取，

instance Applicative Promise where
  pure = trafo2Promise . pure
  fp <*> xp = trafo2Promise $ promise2Trafo fp <*> promise2Trafo xp

现在在这里我们需要证明除其他外

  pure id <*> xp ≡ xp

我们没有手动执行此操作，而是利用该定律已在 ErrorT f Maybe a 中得到证明的事实。 ，所以我们简单介绍一些恒等式:

  trafo2Promise $ promise2Trafo (trafo2Promise $ pure id) <*> promise2Trafo xp
 ≡ trafo2Promise $ pure id <*> promise2Trafo xp

这是 ≡ promise2Trafo xp如果 pure id <*> promise2Trafo xp ≡ promise2Trafo xp ，我们知道这是真的。