Is there any type-safe way to write a function
bi f a b = (f a, f b)
such that it would be possible to use it like this:
x1 :: (Integer, Char)
x1 = bi head [2,3] "45"
x2 :: (Integer, Char)
x2 = bi fst (2,'3') ('4',5)
x3 :: (Integer, Double)
x3 = bi (1+) 2 3.45
? In rank-n-types examples there are always something much simpler like
g :: (forall a. a -> a) -> a -> a -> (a, a)
g f a b = (f a, f b)
Yes, though not in Haskell. But the higher-order polymorphic lambda calculus (aka System F-omega) is more general:
Here, I write
f {T}for explicit type application and assume a library typed respectively. Something like\a. ais a type-level lambda. Thex2example is more intricate, because it also needs existential types to locally "forget" the other bit of polymorphism in the arguments.You can actually simulate this in Haskell by defining a
newtypeor datatype for every differentmornyou instantiate with, and pass appropriately wrapped functionsfthat add and remove constructors accordingly. But obviously, that's no fun at all.Edit: I should point out that this still isn't a fully general solution. For example, I can't see how you could type
even in System F-omega. The problem is that the
swapfunction is more polymorphic thanbiallows, and unlike withx2, the other polymorphic dimension is not forgotten in the result, so the existential trick does not work. It seems that you would need kind polymorphism to allow that one (so that the argument tobican be polymorphic over a varying number of types).