3

I was doing one of the homeworks from functional programming course and found some problems understanding monads in Haskell.

So, we were given a type:

data Annotated e a = a :# e
infix 0 :#

The task was to implement some functions with given type signatures, which I did. They pass needed tests (separately):

mapAnnotated :: (a -> b) -> (Annotated e a -> Annotated e b)
mapAnnotated f (x :# w) = f x :# w

joinAnnotated :: Semigroup e => Annotated e (Annotated e a) -> Annotated e a
joinAnnotated ((b :# m) :# n) = b :# m <> n

distAnnotated :: Semigroup e => (Annotated e a, Annotated e b) -> Annotated e (a, b)
distAnnotated (x :# m, y :# n) = (x, y) :# m <> n

However, we were also asked to satisfy following equation:

distAnnotated (p, q) = joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)

I can't quite get my head around so many function applications, so for other types with similar tasks I just did what seemed "natural" and it worked, but here it doesn't and I can't see why, since I don't even see other ways to implement these functions. What am I missing?

2
  • 3
    What justifies the connective "however"? One thing that could justify it would be finding values of p and q for which the equation is not satisfied. Have you? Do you have another reason that you think your implementations and the requested law are in conflict? Nov 21, 2021 at 17:58
  • The reason I think my implementation is incorrect is that we have tests which, well, test this equation (and basic correctness as well) and they fail. I would readily provide examples where the equation doesn't hold, but that would mean my understanding of it (and also the solution, I guess), which is precisely the problem =) Nov 22, 2021 at 12:34

1 Answer 1

2

Let's start with the troublesome equation and systematically substitute the definitions, working it inside-out:

-- Given
mapAnnotated f (x :# w) = f x :# w
joinAnnotated ((b :# m) :# n) = b :# m <> n
distAnnotated (x :# m, y :# n) = (x, y) :# m <> n
p = x :# m
q = y :# n

-- Goal
distAnnotated (p, q) = joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)

-- Right-hand side
joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) q) p)
joinAnnotated (mapAnnotated (\a -> mapAnnotated (\b -> (a, b)) (y :# n)) (x :# m))
joinAnnotated (mapAnnotated (\a -> (\b -> (a, b)) y :# n) (x :# m))
joinAnnotated (mapAnnotated (\a -> (a, y) :# n) (x :# m))
joinAnnotated (mapAnnotated (\a -> (a, y) :# n) (x :# m))
joinAnnotated ((\a -> (a, y) :# n) x :# m)
joinAnnotated (((x, y) :# n) :# m)
(x, y) :# n <> m
-- Left-hand side
distAnnotated (p, q)
distAnnotated (x :# m, y :# n)
(x, y) :# m <> n
-- LHS /= RHS

The problem, therefore, is that distAnnotated combines the annotations in a different order than joinAnnotated (m <> n versus n <> m). The usual way to make them agree is changing joinAnnotated so that the outside annotation comes first:

joinAnnotated ((b :# m) :# n) = b :# n <> m

This fits both the natural sequencing of computations in the monadic bind (m >>= f = joinAnnotated (mapAnnotated f m)) and the conventional left-to-right order of applicative effects (p <*> q = ap p q = mapAnnotated (\(f, a) -> f a) (distAnnotated (p, q))).

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.