Re: problems with impredicativity
Am Montag, den 07.11.2011, 14:49 +0200 schrieb Wolfgang Jeltsch: > Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagne...@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. Best wishes, Wolfgang ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: problems with impredicativity
Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagne...@seas.upenn.edu:
> Quoting wagne...@seas.upenn.edu:
>
> > Quoting Wolfgang Jeltsch :
> >
> >> this code is accepted by GHC 7.0.4:
> >>
> >> 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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: problems with impredicativity
Wolfgang
Dimitrios, Stephanie and I spent a long time trying to come up with a decent
story for impredicative polymorphism (which would let you use types like
[forlall a. a->a]), wrote several papers about it, and even implemented one
version in GHC (hence -XImpredicativeTypes).
However the implementation was Just Too Complicated, and its specification was
too unpredictable. So during the last major overhaul of the type inference
engine, I took most of it out.
The most promising approach is, I think, Dimitrios and Claudio's QML idea
(http://research.microsoft.com/en-us/um/people/crusso/qml/). It's less
ambitious than our earlier schemes, but it is much simpler.
GHC currently implements a kind of half-way house. We have simply not devoted
serious attention to the story for impredicative types, yet. Too busy with
type functions and other stuff that has seemed more immediately useful. So I'm
afraid I make no warranty for a sensible, predicable behaviour when you are
using impredicativity.
If you care about this, add yourself to the cc list for the ticket
http://hackage.haskell.org/trac/ghc/ticket/4295
explain why it's important to you, and attach a test case showing the kind of
thing you wanted to be able to do. The more motivating examples, the greater
the incentive to fix it.
Simon
| -Original Message-
| From: glasgow-haskell-users-boun...@haskell.org
[mailto:glasgow-haskell-users-
| boun...@haskell.org] On Behalf Of Wolfgang Jeltsch
| Sent: 04 November 2011 22:13
| To: glasgow-haskell-users@haskell.org
| Subject: problems with impredicativity
|
| Hello,
|
| this code is accepted by GHC 7.0.4:
|
| > {-# LANGUAGE ImpredicativeTypes #-}
| >
| > polyId :: (forall a. a) -> a
| > polyId x = x
| >
| > polyIdMap :: [forall a. a] -> [forall a. a]
| > polyIdMap xs = fmap polyId xs
|
| 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?
|
| Best wishes,
| Wolfgang
|
|
| ___
| Glasgow-haskell-users mailing list
| Glasgow-haskell-users@haskell.org
| http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: problems with impredicativity
Quoting wagne...@seas.upenn.edu:
Quoting Wolfgang Jeltsch :
this code is accepted by GHC 7.0.4:
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
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: problems with impredicativity
Quoting Wolfgang Jeltsch :
this code is accepted by GHC 7.0.4:
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)]
~d
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
problems with impredicativity
Hello,
this code is accepted by GHC 7.0.4:
> {-# LANGUAGE ImpredicativeTypes #-}
>
> polyId :: (forall a. a) -> a
> polyId x = x
>
> polyIdMap :: [forall a. a] -> [forall a. a]
> polyIdMap xs = fmap polyId xs
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?
Best wishes,
Wolfgang
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
