[Haskell-cafe] Re: Are arbitrary rank types and existentials equivalent?

On 11/09/08 17:04, Loup Vaillant wrote: [snip]

Err, where can I find such texts? I don't even understand "intuitionistic predicate logic" :-( I just googled that phrase and got many hits. I think metaprl implements something like that:

http://metaprl.org/default.html I've often wondered about haskell and metaprl. I know metprl has something like a hierarchy of types and that's used to avoid Russell's paradox. I also remember reading somewhere (can't remember where) that there was something in category theory that had a hierarchy of categories. Maybe someone else can provide more details.