Browse thread
Predicativity?
- Wei Hu
[
Home
]
[ Index:
by date
|
by threads
]
[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
[ 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!