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
