($) 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-boun...@haskell.org] On Behalf Of Tyson | Whitehead | Sent: 10 February 2015 23:20 | To: Dan Doel | Cc: haskell@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
