Re: [Haskell-cafe] The difference between ($) and application
Derek Elkins
Personally, I would mind ($) being magical. One of the nice things about Haskell is there is practically no magic. The last thing I want is Haskerl (http://www.dcs.gla.ac.uk/~partain/haskerl.html). runST simply had a rank-2 type that is not expressible in Haskell 98, it seems getting ($) to "work" would be qualitatively different.
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. Jonathan Cast
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
participants (2)
-
hancock＠spamcop.net -
Jon Cast