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
signature.asc
Description: Digital signature
_______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
