problems with impredicativity
wagnerdm at seas.upenn.edu
wagnerdm at seas.upenn.edu
Sat Nov 5 01:16:22 CET 2011
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?
>
> Yep, fix the type signature. There is no type you can substitute for
> "a" in "Maybe a" that results in "forall a. Maybe a". But GHC
> accepts the same code with the following type signature, which
> should make clear what I mean:
>
> polyIdMap :: [forall a. Maybe a] -> [Maybe (forall a. a)]
It occurred to me that you may have been attempting to do something
else, so perhaps I fired off my first reply too quickly. Another
interpretation is that the type of polyIdMap is correct, but the type
of polyId isn't.
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)
The first means: first, choose a monomorphic type, then specialize the
first argument to that monomorphic type. The second means: take a
polymorphic value, then return it, delaying the choice of a
monomorphic type until later. (And, again ideally, any unbound
variables would implicitly put their "forall" at the top level, as in
the first signature above.) If this distinction existed, then your
polyIdMap would be fully compatible with a polyId having the second
type signature.
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. The only way I know of to prevent this is to make a
newtype "barrier". 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.)
~d
More information about the Glasgow-haskell-users
mailing list