There is no special type for ($). The name is simply special cased in the compiler. The rule is something like: Whenever you see: f Prelude.$ x instead try to type check: f x That may not be the exact behavior, but it's close. To fix (.) (in a similar fashion) you would have to have a similar rule, like: Whenever you see: f Prelude.. g instead try to type check: \x -> f (g x) -- Dan On Tue, Feb 10, 2015 at 6:19 PM, Tyson Whitehead <twhitehead@gmail.com> wrote:
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