lifting functions to tuples?
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) which does, in fact, compile. A very odd type is inferred: liftTup :: forall b1 b a1 a. (forall a2 b2. a2 -> b2) -> (a, a1) -> (b, b1) I call this odd because there's no mention of the type dependencies inherent in the actual function. However, any attempt to apply it to a polymorphic function results in the following errors: random.hs:17: Could not deduce (Num b) from the context () arising from use of `inc' at random.hs:17 Probable fix: Add (Num b) to the expected type of an expression In the first argument of `liftTup', namely `inc' In the definition of `tupInc': tupInc = liftTup inc random.hs:17: Inferred type is less polymorphic than expected Quantified type variable `b' is unified with another quantified type variable `a' In the first argument of `liftTup', namely `inc' In the definition of `tupInc': tupInc = liftTup inc which seems to be a direct consequence of the odd derived type. However, I can't think of a way to write a better one. The problem, as far as I can tell, is that there's no way in the type system to deal in type transformations, i.e. apply the conversion implied by (a -> b) to a given type a' to produce the appropriate b'. Thoughts? Abe
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@cl.cam.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
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.
Well, it is possible in Haskell. It works even in Hugs! {-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-} class Funnable a b | a->b where f:: a -> b instance Funnable Bool Int where f = fromEnum instance Funnable Char Float where f = fromRational . toRational . fromEnum class LP a b c d where liftf:: (a, b) -> (c, d) instance (Funnable a c, Funnable b d) => LP a b c d where liftf (a,b) = (f a, f b) Main> liftf (True,'z') (1,122.0)
On Tue, Nov 18, 2003 at 05:56:19PM -0800, oleg@pobox.com wrote:
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.
Well, it is possible in Haskell. It works even in Hugs!
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances #-}
class Funnable a b | a->b where f:: a -> b
instance Funnable Bool Int where f = fromEnum instance Funnable Char Float where f = fromRational . toRational . fromEnum
class LP a b c d where liftf:: (a, b) -> (c, d)
instance (Funnable a c, Funnable b d) => LP a b c d where liftf (a,b) = (f a, f b)
Main> liftf (True,'z') (1,122.0)
This seems different from what Abraham Egnor asked for, because it allows one to provide many different implementations for f. It corresponds more closely to
liftTup' (f1, f2) (a, b) = (f1 a, f2 b)
which is of course typable with in Haskell. Main> liftTup' (fromEnum, fromRational . toRational . fromEnum) (1, 122.0) (1,122.0) -- Sebastien
The problem: liftTup f (a, b) = (f a, f b) of the signature liftTup:: ?? -> (a,b) -> (c,d) Again, it is possible to write this in Haskell with common extensions
{-# OPTIONS -fglasgow-exts #-}
import Data.Dynamic import Data.Maybe
liftp f (a,b) = ((fromJust . fromDynamic . f . toDyn) a, (fromJust . fromDynamic . f . toDyn) b)
*Main> :t liftp forall a2 a a3 a1. (Typeable a, Typeable a1, Typeable a2, Typeable a3) => (Dynamic -> Dynamic) -> (a1, a3) -> (a, a2)
f1 x | isJust (fromDynamic x::(Maybe Int)) = let y = fromJust $ fromDynamic x in toDyn $ (toEnum (y + 1)::Char) f1 x | isJust (fromDynamic x::(Maybe Float)) = let y::Float = fromJust $ fromDynamic x in toDyn $ (round(y + 1)::Int) f1 x = x
*Main> liftp f1 (65::Int,1.0::Float) :: (Char,Int) ('B',2)
f2 x | isJust (fromDynamic x::(Maybe Bool)) = let y = fromJust $ fromDynamic x in toDyn $ ((toEnum (if y then 42 else 65))::Char) f2 x | isJust (fromDynamic x::(Maybe ())) = let () = fromJust $ fromDynamic x in toDyn $ (2.5::Float) f2 x = x
*Main> liftp f2 (True,()) :: (Char,Float) ('*',2.5) *Main> liftp f2 (False,()) :: (Char,Float) ('A',2.5) *Main> liftp f2 (False,1::Int) :: (Char,Int) ('A',1) As has been discussed on this list on many occasions, Dynamic (and the accompanied safe coerce) can be implemented in Haskell98 plus existentials and multi-parameter classes with functional dependencies. As a matter of fact, translating (a,b) into (c,d) doesn' seem to be much different than the generic mapping. I think Strafunsky can express such a transformation trivially. Right?
Again, I think what you propose is different from what was asked.
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.
On Wed, Nov 19, 2003 at 05:25:19PM -0800, oleg@pobox.com wrote:
*Main> :t liftp forall a2 a a3 a1. (Typeable a, Typeable a1, Typeable a2, Typeable a3) => (Dynamic -> Dynamic) -> (a1, a3) -> (a, a2)
Here there is no visible relation between the types in the first tuple and the types in the second tuple. The ``type transformation implied in the function to be lifted'' is not reflected in the type of liftp. I think an example of what Abraham Egnor asked for is:
f1 :: a -> Maybe a f1 x = Just x
with desired type (Maybe Int, Maybe Bool) for the expression liftTup f1 (1, True). Yet another example is
data T a = T (a, a -> T a)
f2 :: T a -> T a f2 (T (repr, m)) = m repr
with desired type (T a, T b) -> (T a, T b) for liftTup f2, so that one can for example have
o1 :: Int -> T Int o1 x = T (x, \ x -> o1 (x * 2))
o2 :: Float -> T Float o2 x = T (x, \ x -> o2 (x * 2.0))
v = liftTup f2 (o1 1, o2 1.0)
One could expect v to have type (T Int, T Float), but I don't think the type system of Haskell can handle these simple, uncontrived examples. I don't intend this as a criticism, merely a fact. Of course, one can always defeat the static type system when it gets in the way, using Dynamics, as you demonstrated. -- Sebastien
In case this is of interest, there is another novel way that a language might support liftTup in full generality. Example code:
LiftTup(f:function)(a:f.dom,b:f.dom)={f(a),f(b)} f(x:int)=x+1
LiftTup(f)(3,7) {4,8}
LiftTup(caps)("Hello","Goodbye") {"HELLO","GOODBYE"}
Here, the type system supports full set-theory-style subtyping, with functions subtyping such that a->b <: c->d iff b<:d and c<:a; an empty type "false" containing no elements, and the "function" type the type of functions with empty domain and thus a supertype of every function type. Thus "LiftTup" above takes a parameter f which may be a function of any domain and range. The "f.dom" notation extracts the (dependent) domain type of the function f, which depends on the actual function being passed. Thus the code above is statically typecheckable, and the program, i.e. LiftTup(caps)(3,7) would fail, because "caps" is a function from strings (arrays/tuples of characters) to strings. Though, in my language, tuples are merely dependent-typed arrays of known size, which themselves are a subtype of the type of dependent-typed arrays of unknown (i.e. existentially quantified) size, which are expressed syntacticall as, i.e. []:int. So the above can be rewritten more generally:
Map(f:function)(a[]:dom.f)=array(i:nat<a.len)f(a) Map(f)(3,7,9,12) {4,8,10,13}
Where the "array" notation is an array lambda expression, and a.len extracts the length of an unknown-sized array. This language allows quite a bit more generality and type precision in function and data type definitions, though code tends to lack the conciseness made possible by Haskell type deduction. -Tim ----- Original Message ----- From: <oleg@pobox.com> To: <sebc@macs.hw.ac.uk> Cc: <haskell@haskell.org>; <aegnor@antioch-college.edu>; <Jon.Fairbairn@cl.cam.ac.uk> Sent: Wednesday, November 19, 2003 8:25 PM Subject: Re: lifting functions to tuples?
The problem:
liftTup f (a, b) = (f a, f b)
of the signature liftTup:: ?? -> (a,b) -> (c,d)
Again, it is possible to write this in Haskell with common extensions
{-# OPTIONS -fglasgow-exts #-}
import Data.Dynamic import Data.Maybe
liftp f (a,b) = ((fromJust . fromDynamic . f . toDyn) a, (fromJust . fromDynamic . f . toDyn) b)
*Main> :t liftp forall a2 a a3 a1. (Typeable a, Typeable a1, Typeable a2, Typeable a3) => (Dynamic -> Dynamic) -> (a1, a3) -> (a, a2)
f1 x | isJust (fromDynamic x::(Maybe Int)) = let y = fromJust $ fromDynamic x in toDyn $ (toEnum (y + 1)::Char) f1 x | isJust (fromDynamic x::(Maybe Float)) = let y::Float = fromJust $ fromDynamic x in toDyn $ (round(y + 1)::Int) f1 x = x
*Main> liftp f1 (65::Int,1.0::Float) :: (Char,Int) ('B',2)
f2 x | isJust (fromDynamic x::(Maybe Bool)) = let y = fromJust $ fromDynamic x in toDyn $ ((toEnum (if y then 42 else 65))::Char) f2 x | isJust (fromDynamic x::(Maybe ())) = let () = fromJust $ fromDynamic x in toDyn $ (2.5::Float) f2 x = x
*Main> liftp f2 (True,()) :: (Char,Float) ('*',2.5) *Main> liftp f2 (False,()) :: (Char,Float) ('A',2.5) *Main> liftp f2 (False,1::Int) :: (Char,Int) ('A',1)
As has been discussed on this list on many occasions, Dynamic (and the accompanied safe coerce) can be implemented in Haskell98 plus existentials and multi-parameter classes with functional dependencies.
As a matter of fact, translating (a,b) into (c,d) doesn' seem to be much different than the generic mapping. I think Strafunsky can express such a transformation trivially. Right?
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
On Tue, 2003-11-18 at 15:46, 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.
How about this: liftTup :: (forall a. a -> f a) -> (x, y) -> (f x, f y) liftTup f (x,y) = (f x, f y) Or ghc can infer the type if you write it like this: liftTup (f::forall a.a ->f a) (x::x,y::y) = (f x::f x, f y::f y) or simply: liftTup (f::forall a.a ->f a) (x,y) = (f x, f y) It works too! (ghci -fglasgow-exts)
liftTup Just (1, 'c') (Just 1,Just 'c')
Duncan
That only works for type constructors (or similar encapsulation functions), but not for any sort of a -> b functions, i.e. (+1).
How about this:
liftTup :: (forall a. a -> f a) -> (x, y) -> (f x, f y) liftTup f (x,y) = (f x, f y)
Or ghc can infer the type if you write it like this:
liftTup (f::forall a.a ->f a) (x::x,y::y) = (f x::f x, f y::f y)
or simply:
liftTup (f::forall a.a ->f a) (x,y) = (f x, f y)
It works too! (ghci -fglasgow-exts)
liftTup Just (1, 'c') (Just 1,Just 'c')
Duncan
_______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (6)
-
Abraham Egnor -
Duncan Coutts -
Jon Fairbairn -
oleg＠pobox.com -
sebc＠macs.hw.ac.uk -
Tim Sweeney