[Haskell] Rank-N types with (.) composition

[Simon Peyton Jones]

($) has its own *typing rule*; it does not have a special type.  It's very ad hoc, but ($) is used so much to decrease parens that (e1 $ e2) is almost special syntax!

At the moment the *only* robust way to pass a polymorphic function to a polymorphic function (here, you are passing Wrap to (.)) is to wrap it in a newtype, much as Wrap does.

I have made several forays into the impredicative swamp, and barely made it back to the shore alive.  I think that, at least in the context of Haskell, the trick is to be less ambitious, something like QML.

Since this comes up regularly, I've started a wiki page to explain the issues:
  https://ghc.haskell.org/trac/ghc/wiki/ImpredicativePolymorphism

Please do improve it.

Simon



|  -----Original Message-----
|  From: Haskell [mailto:haskell-bounces at haskell.org] On Behalf Of Tyson
|  Whitehead
|  Sent: 10 February 2015 23:20
|  To: Dan Doel
|  Cc: haskell at haskell.org
|  Subject: Re: [Haskell] Rank-N types with (.) composition
|  
|  On February 10, 2015 16:28:56 Dan Doel wrote:
|  > Impredicativity, with regard to type theories, generally refers to
|  > types being able to quantify over the collection of types that they
|  > are then a part of. So, the judgment:
|  >
|  >     (forall (a :: *). a -> a) :: *
|  >
|  > is impredicative, because we have a type in * that quantifies over
|  all
|  > types in *, which includes itself. Impredicativity in general refers
|  > to this sort of (mildly) self-referential definition.
|  
|  Thanks Dan and David,
|  
|  That was informative.  Also very interesting that ($) is a special
|  case.  I tried this
|  
|   newtype Wrap = Wrap { extract :: forall f. Functor f => f Int }
|  
|   trip'' :: Wrap -> Wrap
|   trip'' a = Wrap $ extract a
|  
|  and the compiler was happy.  Wrapping ($) as ($') gave an error as you
|  implied it would
|  
|   trip''' :: Wrap -> Wrap
|   trip''' a = Wrap $' extract a
|       where ($') = ($)
|  
|  With regard to my earlier comment about translating the (.) version
|  
|   trip' :: Wrap -> Wrap
|   trip' = Wrap . extract
|  
|  to core, I can see it's actually okay.  A most you may need is a
|  lambda to float the implicit parameters backwards
|  
|   trip' :: Wrap -> Wrap
|   trip' = Wrap . (\a f fDict -> extract f fDict a)
|  
|  as GHC seems to always float them as far leftward as possible
|  
|   extract :: Functor f => Wrap -> f Int
|  
|  I take it there are no user supplied types a person can give to
|  overcome the predicative assumption?
|  
|  Out of curiosity, how would you write the special internal type that
|  ($) has that separates it from ($') above?
|  
|  Thanks!  -Tyson
|  _______________________________________________
|  Haskell mailing list
|  Haskell at haskell.org
|  http://www.haskell.org/mailman/listinfo/haskell