Observing isomorphism and then proving them as Monad

Question

This question is related to this answer.

There is a type named Promise:

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

It is stated that:

Promise f a ≅ Maybe (Either f a)

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) ?

Answer 1

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

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

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

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