>>>>> Jon Cast wrote (on Tue, 14 Dec 2004 at 22:02):
> No. All that is needed for ($) to work is impredicativity (or, more
> precisely, for the foralls in ($)'s type to be impredicative). That is
> something that could easily be implemented in a compiler. I'm not clear
> on why it hasn't been, but the type system, in relation to an
> arbitrary-rank predicative system, is no more of a jump that higher-rank
> types were.
This sounds interesting and I'd like to understand it.
* The rank of a type is the nesting depth of quantifiers
over types, isn't it? Nested quantifiers can be understood
either predicatively (with ramified universe types) or impredicatively.
* ($) is the identity function restricted to "functions-in-general" ie
the type FIG = forall a, b . (a -> b) -> a -> b
You are saying (?)
* The type of ($) cannot be expressed predicatively.
(It seems perfectly expressed by FIG. But you could
say that FIG is really (forall a, b :: V_n . ...)
which is not a type because it contains a parameter.
But there is really no parameter, the subscripts are just a way
of ensuring the formula is properly stratified.
Or something to do with ($) being self applicable??
* ?? What we have in implemented type systems is arbitrary-rank
predicative type quantification. (Strewth!)
* It would have been easy instead to implement impredicative
quantification over types.
Sorry if this is hopelessly wrong.
Peter Hancock
_______________________________________________
Haskell-Cafe mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell-cafe
