Enlico
Enlico

Reputation: 28490

Is there any signature that can make "both" defined as "both f = bimap f f" work with heterogeneous pairs?

This works

> bimap succ succ (1, 'a')
(2, 'b')

but this doesn't

> both f = bimap f f
> both succ (1, 'a')

<interactive>:11:12: error:
    • No instance for (Num Char) arising from the literal ‘1’
    • In the expression: 1
      In the second argument of ‘both’, namely ‘(1, 'a')’
      In the expression: both succ (1, 'a')

It's clear that in the first case, the polymorphic succ is deduced (Enum b, Num b) => b -> b and Char -> Char respectively, whereas in the second case, succ must have the same type for both usages, so we end up with that error.

Is making both work just impossible? If so, why?
Or is it just a matter of writing the magic signature?

I played around a few minutes, but without luck (I've gone through this and other sources, but I haven't really fully grasped the topic of existential types, if they are relevant here). As much as this compiles

both :: forall (f :: * -> *) a b. (forall c. f c -> f c) -> (a, b) -> (f a, f b)
both f (a, b) = (f undefined, f undefined)

and HLS tells me that me that the two undefineds have type f a and f b respectively, as soon as I write a and b in their place, I get this error

<interactive>:3:20: error:
    • Couldn't match expected type ‘f a’ with actual type ‘a’
      ‘a’ is a rigid type variable bound by
        the type signature for:
          both :: forall (f :: * -> *) a b.
                  (forall c. f c -> f c) -> (a, b) -> (f a, f b)
        at <interactive>:2:1-80
    • In the first argument of ‘f’, namely ‘a’
      In the expression: f a
      In the expression: (f a, f b)
    • Relevant bindings include
        a :: a (bound at <interactive>:3:9)
        f :: forall c. f c -> f c (bound at <interactive>:3:6)
        both :: (forall c. f c -> f c) -> (a, b) -> (f a, f b)
          (bound at <interactive>:3:1)

<interactive>:3:25: error:
    • Couldn't match expected type ‘f b’ with actual type ‘b’
      ‘b’ is a rigid type variable bound by
        the type signature for:
          both :: forall (f :: * -> *) a b.
                  (forall c. f c -> f c) -> (a, b) -> (f a, f b)
        at <interactive>:2:1-80
    • In the first argument of ‘f’, namely ‘b’
      In the expression: f b
      In the expression: (f a, f b)
    • Relevant bindings include
        b :: b (bound at <interactive>:3:12)
        f :: forall c. f c -> f c (bound at <interactive>:3:6)
        both :: (forall c. f c -> f c) -> (a, b) -> (f a, f b)
          (bound at <interactive>:3:1)

Upvotes: 1

Views: 93

Answers (0)

Related Questions