On Tue, Nov 18, 2003 at 04:34:43PM +0000, Jon Fairbairn wrote:
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.
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')
It can also be straightforwardly expressed in a type system that has intersection types: liftTup :: ((b -> b') ^ (c -> c')) -> (b, c) -> (b', c') where '^' is the intersection type constructor. That is in fact the principal typing for liftTup, and it can be automatically inferred. -- Sebastien