Re: lifting functions to tuples?
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:nata.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: [EMAIL PROTECTED]
To: [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]; [EMAIL PROTECTED];
[EMAIL PROTECTED]
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
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: lifting functions to tuples?
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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: lifting functions to tuples?
On Tue, Nov 18, 2003 at 05:56:19PM -0800, [EMAIL PROTECTED] 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
signature.asc
Description: Digital signature
___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
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
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell
Re: lifting functions to tuples?
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, [EMAIL PROTECTED] 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 signature.asc Description: Digital signature ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
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 ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: lifting functions to tuples?
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 [EMAIL PROTECTED] ___ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
Re: lifting functions to tuples?
On Tue, Nov 18, 2003 at 04:34:43PM +, 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
