lifting functions to tuples?

[sebc at macs.hw.ac.uk]

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-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://haskell.org/pipermail/haskell/attachments/20031118/7737e57c/attachment.bin