lifting functions to tuples?

[Jon Fairbairn]

On 2003-11-18 at 10:46EST "Abraham Egnor" wrote:
> The classic way to write a lift function for tuples is, of course:
> 
> liftTup f (a, b) = (f a, f b)
> 
> which has a type of (a -> b) -> (a, a) -> (b, b).  I've been wondering if
> it would be possible to write a function that doesn't require the types in
> the tuple to be the same, just that the types in the second tuple are the
> result of applying the type transformation implied in the function to be
> lifted to the types in the first tuple.  Now, in Haskell98, this isn't
> possible because of the monomorphism restriction; however, ghc
> conveniently has a way to disable that.  However, I'm still having
> problems figuring out if it's even doable within the current constraints
> of the glasgow-extended type system.  One possibility I tried is:
> 
> liftTup (f :: forall a b. a -> b) (p, q) = (f p, f q)

Note that the type you are requiring for f is equivalent to

   forall a . a -> forall b . b 

which rather limits the possible values for f. Another
possibility would be

   lifTup:: (forall a. a -> b) -> (c, d) -> (b,b)

but that requires the f to be polymorphic and that the
result has elements of the same type.

What you want is that f be applicable to both b and c,
giving results b' and c', but if b and c happen to be the
same type then f need not be polymorphic. I don't think you
can express this in ghc's type system. You'd have to have
bounded quantification:

lifTup :: 
forall c, a >= c, b >= c, d, a'<=d, b'<= d. (c -> d) -> (a,b)->(a',b')

which is monstrous even if I've managed to get it right!

 Jón


-- 
Jón Fairbairn                                 Jon.Fairbairn at cl.cam.ac.uk