Lifting to the limit

Saswat Anand iscp9157@nus.edu.sg
Fri, 16 Feb 2001 21:45:32 +0800


Dear All,
    I have this following simplified  problem. Please help.

type Formula  a b = a -> b
type Env = (Integer,Char)

fun :: Formula Integer Integer
fun n = n+1

sun :: Formula Char Integer
sun c = toInteger.ord c

I want to be able to write 
(sun + fun) (2,'a')   
(fun  + sun) (2,'a')

both of which should be equal to (sun 'a' + fun 2)
   
So I did this:

lift2 :: (a -> b -> c) -> Formula d a -> Formula e b -> Formula Env c
lift2 f a1 a2 = \env -> f  ( (lift a1) n )   ( (lift a2) n )
-- Here hugs gives error

class Lift a where
 lift :: Formula a b -> Formula Env b

instance Lift Char where
 lift f = \(i,c) -> f c

instance Lift Integer where
 lift f =\(i,c) -> f i


With this, hugs (with extensions enabled) gives following error: 

Cannot justify constraints in explicitly typed binding
***Expression        : lift2
***Type                 : (a -> b -> c) -> Formula d a -> Formula e b ->
Formula Env c
***Given Constraint: ()
***Constraints       : (Lift d, Lift e)


Any help is very much appreciated.

Thanks,
Saswat