problems with impredicativity
Wolfgang Jeltsch
g9ks157k at acme.softbase.org
Mon Nov 7 13:49:44 CET 2011
Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagnerdm at seas.upenn.edu:
> Quoting wagnerdm at seas.upenn.edu:
>
> > Quoting Wolfgang Jeltsch <g9ks157k at acme.softbase.org>:
> >
> >> this code is accepted by GHC 7.0.4:
> >> <snip>
> >> However, this one isn?t:
> >>
> >>> {-# LANGUAGE ImpredicativeTypes #-}
> >>>
> >>> polyId :: (forall a. Maybe a) -> Maybe a
> >>> polyId x = x
> >>>
> >>> polyIdMap :: [forall a. Maybe a] -> [forall a. Maybe a]
> >>> polyIdMap xs = fmap polyId xs
> >>
> >> Is there a way to make it accepted?
>
> […]
>
> The first thing to observe is that, ideally, the following two types
> would mean slightly different things:
>
> polyId :: forall b. (forall a. Maybe a) -> Maybe b
> polyId :: (forall a. Maybe a) -> (forall b. Maybe b)
>
> […]
>
> Unfortunately, in GHC, these two types do not mean different things:
> "forall"s on the result side of an arrow are silently floated to the
> top level, even if you explicitly choose to put them later in your
> type annotation.
That’s the problem. I could have written the second type in the type
signature, which would directly express my intension, but I didn’t,
since GHC silently transforms it into the first type anyway.
> The only way I know of to prevent this is to make a newtype "barrier".
This is what I already thought of worth trying.
> For example, the following works:
>
> newtype PolyMaybe = PolyMaybe (forall a. Maybe a)
>
> polyId :: PolyMaybe -> PolyMaybe
> polyId x = x
>
> polyIdMap :: [PolyMaybe] -> [PolyMaybe]
> polyIdMap xs = fmap polyId xs
>
> Then, later, you can unwrap the PolyMaybe -- but only when you're
> ready to turn it into a monomorphic Maybe! (Note that none of these
> things is using ImpredicativeTypes, which is what made me jump to my
> first, probably mistaken impression of what you were trying to do.
> Rank2Types is enough for the above to compile.)
I shouldn’t need impredicativity in the result, so I’ll try this route.
> ~d
Best wishes,
Wolfgang
More information about the Glasgow-haskell-users
mailing list