By observing isomorphism and then proving them as a Monad

Question

This question is related to the answer.

There is a type called Promise :

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

It is alleged that:

 Promise fa ≅ Maybe (Either fa) 

Now I can not understand the above expression. How are they kind of equivalent and isomorphic (and from this how can you conclude that this is a monad)?

Answer 1

Two types A and B isomorphic if there are two functions a2b :: A -> B and b2a :: B -> A such that a2b . b2a ≡ id a2b . b2a ≡ id and b2a . a2b ≡ id b2a . a2b ≡ id . This is easy to prove in this example: the two functions have basically the same sentences as the = sides turned around, for example,

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

therefore compiling functions in any order gives you an identity function. The most important feature of isomorphism is that a2b x ≡ a2b y holds exactly if f x ≡ y .

Now, how does this help prove the laws of styles? Again taken from the example,

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

Now we need to prove, among other things,

  pure id <*> xp ≡ xp 

Instead of doing it manually, we use the fact that this law has already been proved for ErrorT f Maybe a , so we just 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, as we know, is true.

Answer 2

A value of type Promise fa can be three different:

• A value of type f , with the PendingPromise constructor.
• A value of type a , with the ResolvedPromis constructor,
• or not value with BrokenPromise constructor.

Similarly, the Maybe (Either fa) value can be three:

• A value of type f , with the constructor Just . Left Just . Left
• A value of type a , with the constructor Just . Right Just . Right
• No value, with the Nothing constructor.

In this sense, types are isomorphic. The reason this is not entirely true in Haskell is due to undefined (bottomoms) values, but you can ignore them to make life easier.

Maybe (Either fa) can also be seen as EitherT f (Maybe a) , which is an instance of Monad .

Answer 3

You can easily map Promise fa to Maybe (Either fa) as follows:

• PendingPromise f -> Just (Left f)
• ResolvedPromise a -> Just (Right a)
• BrokenPromise -> Nothing

Given that both Maybe and Either are Monad instances, the Promise expression can be expressed as a monad.

A possible implementation may be:

 instance Monad (Promise f) where return a = ResolvedPromise a BrokenPromise >>= _ = BrokenPromise PendingPromise a >>= _ = PendingPromise a ResolvedPromise a >>= f = fa 

Live demo

Answer 4

There are three possibilities for Maybe (Either fa) :

 Just (Left f) | Just (Right a) | Nothing 

It is isomorphic to Promise fa .

This is the same as

 EitherT f (Maybe a) 

which is also a monad.