[Haskell-cafe] The difference between ($) and application

[Peter G. Hancock]

>>>>> 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