Version française
Home     About     Download     Resources     Contact us    
Browse thread
Predicativity?
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Wei Hu <weihu@c...>
Subject: Predicativity?
Hello,

Isn't OCaml's polymorphism predicative? Then, why does the following code in 
the interactive toplevel type check?

# let id x = x;;
val id : 'a -> 'a = <fun>
# let f x = (id id) x;;
val f : 'a -> 'a = <fun>

I thought id could not be applied to itself under predicative polymorphism. Is 
my understanding wrong? Can you show an example that doesn't type check in 
OCaml, but would type check under impredicate polymorphism?

Thanks!