higher rank polymorphism

15 Nov 2006

      Hi,

I want to use a rank 2 data type and end up in typ problems that I  
don't understand. I would really appreciate any hints to the  
presented cases or pointers to interesting papers that address the  
background of these problems.

I define the following datatype and a simple function that checks  
whether the list is empty.

data Test = Test (forall a . [a -> a])

null1 :: Test -> Bool
null1 (Test []) = True
null1 (Test _) = False

null2 :: Test -> Bool
null2 (Test l) = null l

null3 :: Test -> Bool
null3 (Test l) =
   case l of
        [] -> True
        _  -> False

For null1 ghc reports the following typeerror:
     Couldn't match expected type `forall a. [a -> a]'
            against inferred type `[a]'
     In the pattern: []
     In the pattern: Test []
     In the definition of `null1': null1 (Test []) = True

while null2 and null3 don't cause errors. I don't understand why  
there is a difference between these definitions of null.

cp1 :: Test -> Test
cp1 (Test l) =
   case l of
        []     -> Test []
        (x:xs) -> Test (x:xs)

cp2 :: Test -> Test
cp2 (Test l) =
   if null l
      then Test []
      else Test (head l:tail l)

For cp1 ghc reports the following typeerror:
     Inferred type is less polymorphic than expected
       Quantified type variable `a' is mentioned in the environment:
         xs :: [a -> a] (bound at UpDownTree.hs:36:10)
         x :: a -> a (bound at UpDownTree.hs:36:8)
     In the first argument of `Test', namely `(x : xs)'
     In the expression: Test (x : xs)
     In a case alternative: (x : xs) -> Test (x : xs)

while for cp2 ghc doesn't report an error. I guess there is a similar  
reason for this error as for the error for null1.

I now want to restrict the polymorphic functions in the data type to  
types for which there is an instance of the type class Eq.

data TestEq = TestEq (forall a . Eq a => [a -> a])

null4 :: TestEq -> Bool
null4 (TestEq l) = null l

For null4 ghc reports the following typeerror:
     Ambiguous type variable `a' in the constraint:
       `Eq a' arising from use of `l' at UpDownClass.hs:37:24
     Probable fix: add a type signature that fixes these type variable 
(s)

I obviously cannot add a constraint that constraints a type variable  
that doesn't occur in the type of null4.

I will be very pleased for any hints.

Regards, Jan

higher rank polymorphism

Jan Christiansen