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)
Louis Wasserman :
Even with ConstraintKinds, I think the barrier is going to be quantifying over the \"type function\" from the arguments to the results. What you want is for f to map a -> b and c -> d, and to take a -> b -> (c, d), but I don't think there's any way to quantify over that relationship with full generality.\n\nSome special cases might be doable, though:\n\n(forall x . cxt x => x -> f x) -> a -> b -> (f a, f b)\n -- e.g. return\n\n(forall x . cxt x => f x -> x) -> f a -> f b -> (a, b)\n -- e.g. snd\n(forall x . cxt x => x -> x) -> a -> b -> (a, b)\n -- e.g. (+1)\n\n\nbut given that you're trying to quantify over more or less arbitrary type functions, I'm not sure you can make that work.",
2012-05-27T07:33:47
FunctorSalad :
{-# LANGUAGE TemplateHaskell #-}\n\nbi f = [| \\a b -> ($f a, $f b)|]\n\n\n \n\nghci> :set -XTemplateHaskell \nghci> $(bi [|head|]) [2,3] \"45\" \n(2,'4')\n\n\n;)",
2012-05-30T02:41:41
Andreas Rossberg :
Yes, though not in Haskell. But the higher-order polymorphic lambda calculus (aka System F-omega) is more general:\n\nbi : forall m n a b. (forall a. m a -> n a) -> m a -> m b -> (n a, n b)\nbi {m} {n} {a} {b} f x y = (f {a} x, f {b} y)\n\nx1 : (Integer, Char)\nx1 = bi {\\a. List a} {\\a. a} {Integer} {Char} head [2,3] \"45\"\n\nx2 : (Integer, Char)\nx2 = bi {\\a . exists b. (a, b)} {\\a. a} {Integer} {Char} (\\{a}. \\p. unpack<b,x>=p in fst {a} {b} x) (pack<Char, (2,'3')>) (pack<Integer, ('4',5)>)\n\nx3 : (Integer, Double)\nx3 = bi {\\a. a} {\\a. a} {Integer} {Double} (1+) 2 3.45\n\n\nHere, I write f {T} for explicit type application and assume a library typed respectively. Something like \\a. a is a type-level lambda. The x2 example is more intricate, because it also needs existential types to locally \"forget\" the other bit of polymorphism in the arguments.\n\nYou can actually simulate this in Haskell by defining a newtype or datatype for every different m or n you instantiate with, and pass appropriately wrapped functions f that add and remove constructors accordingly. But obviously, that's no fun at all.\n\nEdit: I should point out that this still isn't a fully general solution. For example, I can't see how you could type\n\nswap (x,y) = (y,x)\nx4 = bi swap (3, \"hi\") (True, 3.1)\n\n\neven in System F-omega. The problem is that the swap function is more polymorphic than bi allows, and unlike with x2, 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 to bi can be polymorphic over a varying number of types).",
2012-05-30T06:58:05