观察同构,然后将它们证明为Monad

Question

这个问题与这个答案有关.

有一个名为的类型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保持iff 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 xpiff pure id <*> promise2Trafo xp ? promise2Trafo xp,我们知道这是真的.

+1因为这是迄今为止调用反转的唯一答案.我想补充一点,"Applicative"类证明可能更有洞察力地指出(1)`可能(Either fa)`是`Maybe`和`E fither'的组成,以及(2)[作文两个`Applicatives`总是一个'Applicative`也是](http://hackage.haskell.org/package/transformers-0.4.1.0/docs/Data-Functor-Compose.html); 因此同构允许我们简单地为`Promise fa`实现一个`Applicative`实例. (3认同)

Answer 2

类型的值Promise f a可以是三种不同的东西:

同样,值Maybe (Either f a)可以是三件事:

所以在这个意义上,类型是同构的.在Haskell中这不是很正确的原因与undefined值(底部)有关,但你可以忽略它们以使生活更轻松.

Maybe (Either f a)也可以看作EitherT f (Maybe a),这是一个实例Monad.