观察同构，然后证明它们为Monad [英] Observing isomorphism and then proving them as Monad

问题描述

此问题与此答案有关.

有一个名为Promise的类型:

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

据说:

Promise f a ≅ Maybe (Either f a)

现在我不明白上面的表达.他们怎么样 等价的和同构的(从中可以得出结论 是Monad)?

Now I cannot understand the above expression. How are they sort of equivalent and isomorphic (and from that how can you conclude that it is a Monad) ?

推荐答案

如果有两个函数a2b :: A -> B和b2a :: B -> A(例如a2b . b2a ≡ id和b2a . a2b ≡ id)，则两个类型A和B是同构的.在示例中，这很容易证明:这两个函数的子句基本相同，而=的两边都转过来了，例如

Two types A and B are isomorphic if there's two functions a2b :: A -> B and b2a :: B -> A such that a2b . b2a ≡ id and b2a . a2b ≡ id. In the example this is easy to prove: the two functions have basically the same clauses with the sides of = turned around, e.g.

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

因此以任何顺序构成功能都会为您提供身份功能.同构的关键在于，a2b x ≡ a2b y完全保留iff x ≡ y.

so composing the functions in either order gives you the identity function. The crucial thing about an isomorphism is that a2b x ≡ a2b y holds exactly iff x ≡ y.

现在，这如何帮助证明类型定律?再次摘自示例

Now, how does that help proving typeclass laws? Again taken from the example,

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

现在，我们需要在其中进行证明

Now here we need to prove amongst other things

  pure id <*> xp ≡ xp

我们不是手工做这件事，而是利用了该定律已经为ErrorT f Maybe a证明的事实，因此我们仅介绍一些标识:

Instead of doing this by hand, we exploit the fact that this law has already been proven for ErrorT f Maybe a, so we simply introduce some identities:

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

这是≡ promise2Trafo xp iff pure id <*> promise2Trafo xp ≡ promise2Trafo xp，我们知道这是真的.

which is ≡ promise2Trafo xp iff pure id <*> promise2Trafo xp ≡ promise2Trafo xp, which we know is true.

这篇关于观察同构，然后证明它们为Monad的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！