9

Suppose I have a type Pair:

data Pair a = Pair a a

What is the right way to write a monad instance for it? My idea is roughly this:

instance Semigroup a => Semigroup (Pair a) where
  Pair a1 a2 <> Pair b1 b2 = Pair (a1 <> b1)(a2 <> b2)

instance Monad Pair where
  return = pure
  (Pair a b) >>= f = f a <> f b

Is it correct? If so then where to specify that b-type in the Pair b is a semigroup?

Enlico
  • 23,259
  • 6
  • 48
  • 102
Stefan Dorn
  • 569
  • 2
  • 13

5 Answers5

14

Actually, the only correct monad instance of Pair is as follows.

instance Monad Pair where
    m >>= f = joinPair (f <$> m)

joinPair :: Pair (Pair a) -> Pair a
joinPair (Pair (Pair x _) (Pair _ y)) = Pair x y

The reason this is the correct monad instance is because Pair is a representable functor.

instance Representable Pair where
    type Rep Pair = Bool

    index (Pair x _) False = x
    index (Pair _ y) True  = y

    tabulate f = Pair (f False) (f True)

Turns out, for every representable functor (>>=) is equivalent to the following bindRep function.

bindRep :: Representable f => f a -> (a -> f b) -> f b
bindRep m f = tabulate (\a -> index (f (index m a)) a)

If we specialize the bindRep function to Pair we get the following.

bindRep :: Pair a -> (a -> Pair b) -> Pair b
bindRep (Pair x y) f = tabulate (\a -> index (f (index (Pair x y) a)) a)
                     = Pair (index (f x) False) (index (f y) True)
--                          |_________________| |________________|
--                                   |                   |
--                           (1st elem of f x)   (2nd elem of f y)

The following blog post by Adelbert Chang explains it better. Reasoning with representable functors.


Here's another way to prove uniqueness. Consider the left and right identity monad instance laws.

return a >>= k = k a -- left identity law

m >>= return = m     -- right identity law

Now, for the Pair data type return x = Pair x x. Hence, we can specialize these laws.

Pair a a >>= k = k a     -- left identity law

m >>= \x -> Pair x x = m -- right identity law

So, what should the definition of >>= be in order to satisfy these two laws?

Pair x y >>= f = Pair (oneOf [x1, x2, y1, y2]) (oneOf [x1, x2, y1, y2])
    where Pair x1 y1 = f x
          Pair x2 y2 = f y

The oneOf function returns one of the elements of the list non-deterministically.

Now, if our >>= function is to satisfy the left identity law then when x = y then x1 = x2 and y1 = y2 and the result must be Pair (oneOf [x1, x2]) (oneOf [y1, y2]).

Similarly, if our >>= function is to satisfy the right identity law then x1 = y1 = x and x2 = y2 = y and the result must be Pair (oneOf [x1, y1]) (oneOf [x2, y2]).

Hence, if you want to satisfy both laws then the only valid result is Pair x1 y2.

Enlico
  • 23,259
  • 6
  • 48
  • 102
Aadit M Shah
  • 72,912
  • 30
  • 168
  • 299
  • 1
    @dfeuer Updated my answer to prove uniqueness using the monad instance laws. – Aadit M Shah Oct 07 '20 at 01:24
  • You seem to appeal implicitly to parametricity. I imagine this is unavoidable? – dfeuer Oct 07 '20 at 03:11
  • I'm not sure what you mean. – Aadit M Shah Oct 07 '20 at 09:44
  • 2
    Your proof begins with (and hinges critically on) the definition `return x = Pair x x`. This is the only sensible definition in Haskell -- but only because of parametricity. In a non-parametric context, one might wonder whether `return 0 = Pair 1 2; return x = Pair x x` might be a possible choice, say. – Daniel Wagner Oct 07 '20 at 11:01
  • 1
    @DanielWagner I can't prove my intuition but I believe that a non-parametric monad instance of `Pair` would not be able to satisfy all the monad laws. Consider the expression `(m >>= k) >>= h`. If `m >>= k` evaluates to `return x` for some `x` then the entire expression should evaluate to `k x` because of the left identity law. However, if `return x` is not `Pair x x` then `m >>= (\x -> k x >>= h)` could evaluate to something other than `k x`. Hence, it would violate the associativity law. However, I don't know how to prove this hypothesis. Here's a code example. https://jsfiddle.net/zf0eL9jk/ – Aadit M Shah Oct 08 '20 at 04:39
  • 2
    @AaditMShah I suspect both standalone instances of `k x` in your text were intended to be `h x`, right? If so, then I think there's still quite a lot of holes in your argument, it seems to me -- we are asking if a lawful non-parametric definition exists, but all you appear to have argued is that an unlawful non-parametric definition exists. – Daniel Wagner Oct 08 '20 at 07:06
  • @DanielWagner Yes, good catch. It was supposed to be `h x`. – Aadit M Shah Oct 08 '20 at 08:53
  • 1
    For any two monads M, N, the product (M a, N a) is also a monad. The pair (a, a) is a special case where both M and N are identity functors. – winitzki Nov 10 '22 at 13:34
  • @winitzki Whoa, that actually makes the derivation of `>>=` much simpler. Just follow the types. – Aadit M Shah Nov 11 '22 at 05:22
4

Functor and applicative instances are easy. The monad instance has taken a while to me.

data Pair a = Pair a a deriving (Eq, Show)

instance Functor Pair where 
  fmap f (Pair a b) = Pair (f a) (f b)

instance Applicative Pair where 
  pure a = Pair a a
  (Pair f g) <*> (Pair a b) = Pair (f a) (g b)

instance Monad Pair where 
  return = pure
  (Pair a b) >>= f = let Pair a' _ = f a 
                         Pair _ b' = f b
                     in  Pair a' b'

The way I've come to this solution is by applying the monad laws. Easily you can check with an example that identity law doesn't hold if you take Pair a' a'' or Pair b' b'' or Pair a' b' nor Pair a'' b''. So the only solutions must be in the diagonals. Defining

(m >>= f) = Pair (first . f . first $ m) (second . f . second $ m)

where first and second are the obvious ones, you can proof all of the laws.

chepner
  • 497,756
  • 71
  • 530
  • 681
lsmor
  • 4,698
  • 17
  • 38
3

It is possible to make Pair into Monad by having join that takes the diagonal.of the 2×2 square. return has no other choice but replicate its argument. This turns Pair into essentially a fixed length ZipList.

Of course this definition of join discards some data. This may or may not be important.

n. m. could be an AI
  • 112,515
  • 14
  • 128
  • 243
0

A Monad instance may not place any constraints on the type of data it contains (the a here). It must treat that data as fully opaque. I don't think your Pair type admits a Monad instance (or Applicative), because there is no way to turn a pair of pairs into a single pair without either losing some of the data, or using it in some way not permitted by the typeclass definition.

amalloy
  • 89,153
  • 8
  • 140
  • 205
0

Why I am answering

I was curious to know what the practical usages of the Pair a monad are, especially considering that the only valid implementation of (>>=) actually throws away half of the data, so I asked this question.

It turns out that the answer I accepted is a very interesting answer to this question too (and was contained in Daniel Wagner's comment under the present question, but I hadn't noticed it), so I will elaborate it a bit here, because I've learned a lot from it.

The short answer: (a,a) and Bool -> a are the same thing

So the short answer is that the types Pair a, or more simply (a,a), and Bool -> a are isomorphic: feeding a (a,a) to fst/snd is equivalent to feeding a Bool -> a function with True/False (or False/True, it's just a choice). The two isomorphisms are actually shown in the (deleted) answer from Zhiltsoff Igor:

funToPair :: (Bool -> a) -> (a, a)
funToPair f = (f True, f False)

pairToFun :: (a, a) -> Bool -> a
pairToFun (x, y) True = x
pairToFun (x, y) False = y

As a consquence, whichever way Bool -> a is a monad, (a,a)/Pair a is a monad in the same way.

But (a,a)'s Monad throws information away... so does Bool -> a!

What bugged me at this point was that it's so apparent that the Monad instance for (a,a)/Pair a, thoroughly explained in Aadit M Shah's answer, throws away data, whereas the Monad instance for Bool -> a... doesn't...?

Fatally wrong! The Monad instance for r -> a (with generic r, not just Bool) throws away information all the time! How? Let's look at the well known implementation of >>=:

instance Monad ((->) r) where
    f >>= k = \ r -> k (f r) r

Now remember that a function of type x -> y is equivalent to a tuple of type (y,y,...,y) with as many entries as the number of possible values of type x (not y).

What about k? k is a binary function, let's say of type x -> y -> z, so it can be fed with the cartesian product of the values that inhabit the type x and those that inhabit the type of y. If x and y are inhabited by m and n values respectively, then k is equivalent to a tuple of type (z,z,...,z) with as many entries as m*n, and that is the information that comes with k.

Now the question is whether (>>=) makes use of all that information. No, it doesn't! (>>=) is feeding k with only n possible inputs: the second argument r is any value of type x, whereas the first argument is the single value corresponding to r via f.

If we think of mathematical functions, we are saying that, for fixed unary function f: A → B and binary function k: B×A → C, f >>= k is the unary function that does t ∈ A → k(f(t),t) ∈ C, i.e. it's a restriction of k to the curve parametrized by the equations x = f(t) and y = t.

Going back to Bool -> a, the signature of (>>=) specilizes to

(>>=) :: (Bool -> a) -> (a -> Bool -> b) -> Bool -> b
f >>= k = \r -> k (f r) r

which we can rewrite as follows, just to make the obvious more apparent:

(>>=) f k r
  | r == True  = k (f True)  True
  | r == False = k (f False) False
-- remember this

What's obvious in the above? If we feed f >>= k with True, we'll only use f True, thus throwing away the other half of the data, f False. Similarly, if we call (f >>= k) False, we throw away whatever f True is. This way of throwing away half of the information contained in k mirrors exactly what is throw away via the _ placeholders for (a,a) aka Pair a (adaptation from Ismor's answer):

instance Monad Pair where 
  return = pure
  (Pair a b) >>= k = let Pair a' _  = k a
                         Pair _  b' = k b
                     in  Pair a' b'

Indeed, if we define fst' (Pair a _) = a and snd' (Pair _ b) = b (these are mirroring fst and snd for (,)), then (>>=) can be written simply as follows

(>>=) :: Pair a -> (a -> Pair b) -> Pair b
p >>= k = (fst' (k (fst' p)),
           snd' (k (snd' p)))

Which is in my opinion strikingly similar to the code I marked with -- remember this, with fst' mirrors True and snd' mirrors False.

By the way, for the following, let's take note of the type of (>>=) in the case we were allowed to write it for (a,a):

(>>=) :: (a,a) -> (a -> (b,b)) -> (b,b)

What about (a,b) when a and b are the same type?

This was the last doubt I had: since (a,b) is a Monad in b provided a is a Monoid, in the special case that the type b is equal to the type a (and b has to be a Monoid), do we get the same instance as above?

No, the question above is ill-posed, the flaw being in the part "in the special case that the type b is equal to the type a". This hypothesis is simply not possible because for a type constructor to be a Monad, it has to have one and only one free type parameter:

  • (a,b) is made a Monad in the free parameter b, meaning that b will be allowed to vary according to the second argument to (>>=), whereas the type a will stay the same through the (>>=) operator;
  • (a,a) is made a Monad in the free parameter a, meaning that a will be allowed to vary according to the second argument to (>>=), whereas... nothing, that's it, all explained in the previous part of the answer.
Enlico
  • 23,259
  • 6
  • 48
  • 102