problems with impredicativity
g9ks157k at acme.softbase.org
Mon Nov 7 16:21:14 CET 2011
Am Montag, den 07.11.2011, 14:49 +0200 schrieb Wolfgang Jeltsch:
> Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagnerdm at seas.upenn.edu:
> > 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.
Yes, this works. Thank you.
More information about the Glasgow-haskell-users