higher rank polymorphism

Jan Christiansen jac at informatik.uni-kiel.de
Fri Nov 17 03:22:24 EST 2006

Am 16.11.2006 um 13:33 schrieb Tomasz Zielonka:

> On Wed, Nov 15, 2006 at 01:20:43PM +0100, Jan Christiansen wrote:
> I would work, if you used existential quantification, but I am don't
> know if it would be what you want:
> data Test = forall a . Test [a -> a]
> I don't know why you current code doesn't work - sorry.

I want to apply the functions in the list to values of various types  
for example to a value of type String and to a value of type Int.  
Therefore an existential type doesn't work as I see. More precisely I  
want to use a function encoding of a recursive data type in this  
special case of a binary tree, i.e., a datatype

forall b . (b -> (b -> a -> b -> b) -> b)

This type gets an additional b and is packed in a list and this list  
is packed in a data type

data UpDownTree a = UpDownTree (Tree a) (forall b . [b -> (b -> a ->  
b -> b) -> b -> b])

I notice that it would be more straight forward to pull the  
quantifier to the inside of the list. I have seen that the ghc  
documentation calls this impredicative polymorphism. I will take a  
look at the ICFP paper cause at the moment I do not know the  
difference between [(forall a. a -> a)] and forall a . [a -> a].

My implementation already works if I use null, head and tail. But I  
would like to use a type class constraint on b and this doesn't work.  
Furthermore I would like to understand why ghc doesn't report an  
error when I use null, head and tail but reports errors when I use  
pattern matching.

Regards, Jan

More information about the Glasgow-haskell-users mailing list