13

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)
4

4 に答える 4

6 
{-# LANGUAGE TemplateHaskell #-}

bi f = [| \a b -> ($f a, $f b)|]

 

ghci> :set -XTemplateHaskell 
ghci> $(bi [|head|]) [2,3] "45" 
(2,'4')

;）

于 2012-05-30T02:41:41.753 に答える
4

Yes, though not in Haskell. But the higher-order polymorphic lambda calculus (aka System F-omega) is more general:

bi : forall m n a b. (forall a. m a -> n a) -> m a -> m b -> (n a, n b)
bi {m} {n} {a} {b} f x y = (f {a} x, f {b} y)

x1 : (Integer, Char)
x1 = bi {\a. List a} {\a. a} {Integer} {Char} head [2,3] "45"

x2 : (Integer, Char)
x2 = 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)>)

x3 : (Integer, Double)
x3 = bi {\a. a} {\a. a} {Integer} {Double} (1+) 2 3.45

Here, 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.

You 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.

Edit: I should point out that this still isn't a fully general solution. For example, I can't see how you could type

swap (x,y) = (y,x)
x4 = bi swap (3, "hi") (True, 3.1)

even 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.510 に答える
3

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.

Some special cases might be doable, though:

(forall x . cxt x => x -> f x) -> a -> b -> (f a, f b)
 -- e.g. return

(forall x . cxt x => f x -> x) -> f a -> f b -> (a, b)
 -- e.g. snd
(forall x . cxt x => x -> x) -> a -> b -> (a, b)
 -- e.g. (+1)

but 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.963 に答える
2

This is about as close as you're going to get, I think:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
module Data.Function.Bi (bi, Fn(..))

bi :: (Fn i a a', Fn i b b') => i -> a -> b -> (a', b')
bi i a b = (fn i a, fn i b)

class Fn i x x' | i x -> x' where
      fn :: i -> x -> x'

Use it like so:

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, RankNTypes,
             FlexibleInstances, UndecidableInstances #-}
import Data.Function.Bi

data Snd = Snd

instance Fn Snd (a, b) b where
         fn Snd = snd

myExpr1 :: (Int, String)
myExpr1 = bi Snd (1, 2) ("a", "b")
-- myExpr == (2, "b")

data Plus = Plus (forall a. (Num a) => a)

instance (Num a) => Fn Plus a a where
         fn (Plus n) = (+n)

myExpr2 :: (Int, Double)
myExpr2 = bi (Plus 1) (1, 2) (1.3, 5.7)
-- myExpr2 == (3, 6.7)

It's very clunky, but as general as possible.

于 2012-05-27T20:19:06.710 に答える