lifting functions to tuples?

[Tim Sweeney]

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 at pobox.com>
To: <sebc at macs.hw.ac.uk>
Cc: <haskell at haskell.org>; <aegnor at antioch-college.edu>;
<Jon.Fairbairn at 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 at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell