Mon Nov  2 20:41:59 GMT 2009  Ganesh Sittampalam <ganesh@earth.li>
  * build fixes for GHC 6.12
   - bump upper bound of various dependencies
   - remove some uses of impredicativity in preparation for it
     being removed from GHC
   - GADTs extension now needed when they are being matched against as well
     as when they are being defined, so added to .cabal file for witnesses
     build

Attachments

• build-fixes-for-ghc-6_12.dpatch
• unnamed

Petr pointed out this will conflict with several other live submissions so we'll
defer it for now.

I've re-submitted everything apart from the actual code changes to remove
impredicativity in patch112. The removal of impredicativity still needs to be
done before GHC 6.14 so I'm leaving this patch sitting around as a reminder.

Now that a lot of submissions have landed, is it time to revive this patch?

[Just very unsystematically trying to clear this patch tracker]

1 patch for repository darcs-unstable@darcs.net:darcs:

Sat Jun 26 17:30:16 BST 2010  Ganesh Sittampalam <ganesh@earth.li>
  * stop using impredicativity
  This is planned to be removed or changed in GHC 6.14

Attachments

• stop-using-impredicativity.dpatch
• unnamed

On Sat, Jun 26, 2010 at 16:35:22 +0000, Ganesh Sittampalam wrote:
> Sat Jun 26 17:30:16 BST 2010  Ganesh Sittampalam <ganesh@earth.li>
>   * stop using impredicativity
>   This is planned to be removed or changed in GHC 6.14

I'm going to apply this without really understanding it on the grounds
that it looks harmless enough.

stop using impredicativity
--------------------------
>  type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y))
> -subcommutes :: [(String, CommuteFunction)]
> +subcommutes :: [(String, (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y)))]

I'm not clear on why this particular change is necessary and suspect it
just slipped in by accident

Attention Conservation Notice: the rest of this is just Eric learns Haskell

Pain-tolerance Conservation Notice: ... and may be wince-inducing if you
                                    know what you're talking about
 
Impredicativity is explained here in the GHC user docs, but to little
use for me.  On the other hand, the first page of the Boxy Types paper
(linked from those GHC user docs) made matters a little bit clearer,
but I probably still fail to understand.

 * http://www.haskell.org/ghc/docs/6.10.3/html/users_guide/other-type-extensions.html
 * http://research.microsoft.com/en-us/um/people/simonpj/papers/boxy/
 * http://www.haskell.org/pipermail/glasgow-haskell-users/2009-October/017921.html 

My current superficial understanding is that for types that take
variables (eg. Maybe a), impredicativity lets us plug variables with
forall quantifiers to the type constructor (eg. you can write g :: Maybe
(forall a. a))

So an example of a place where we were using this feature is

>  restrictSubpaths :: (RepoPatch p) => Repository p C(r u t) -> [SubPath]
> -                 -> IO (forall t m. FilterTree t m => t m -> t m)

where we're using variables t m quantified (err...) inside IO

> hunk ./src/Darcs/Repository/State.hs 75
> +newtype TreeFilter m = TreeFilter { applyTreeFilter :: forall tr . FilterTree tr m => tr m -> tr m }

This is the main change

>  restrictSubpaths :: (RepoPatch p) => Repository p C(r u t) -> [SubPath]
> -                 -> IO (forall t m. FilterTree t m => t m -> t m)
> +                 -> IO (TreeFilter m)

and a particular example of the change in action.

I'm guessing here we actually never needed that inner forall m in the
first place and were only using impredicativity for t.

The trick to avoid it is just to wrap the arguments to IO up in a type
and give an accessors function using rank N types (nicely explained in
boxy types above as "types with ∀ quantifiers nested inside function
types"), for example, the above

  applyTreeFilter :: TreeFilter m -> (forall tr . FilterTree tr m => tr m -> tr m)

So when we unpack the TreeFilter, we get that

  forall t m. FilterTree t m => t m -> t m

function we wanted.

-- 
Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
PGP Key ID: 08AC04F9

This patch bundle (with 1 patches) was just applied to the repository http://darcs.net/.
This message was brought to you by DarcsWatch
http://darcswatch.nomeata.de/repo_http:__darcs.net_.html#bundle-0c50e7f2922fb37df4e6e671bf8974abb3b9695c

On Wed, 30 Jun 2010, Eric Kow wrote:

> On Sat, Jun 26, 2010 at 16:35:22 +0000, Ganesh Sittampalam wrote:

>>  type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y))
>> -subcommutes :: [(String, CommuteFunction)]
>> +subcommutes :: [(String, (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y)))]
>
> I'm not clear on why this particular change is necessary and suspect it
> just slipped in by accident

No, it is necessary :-) CommuteFunction has an explicit forall - it's just 
a type alias and those get expanded at each use site, so the old code had 
a forall inside the tuple type.

Imagine that pairs are explicitly defined as a Haskell datatype rather 
than being part of the language. The definition might look something like 
this:

data (a, b) = (a, b)

In other words a pair is something that takes two type variables as type 
parameters. As you say in the rest of your review, impredicativity makes 
it legal to instantiate those variables with types that have a top-level 
forall. Without impredicativity, that isn't legal so we have to change it 
somehow. It turns out that in this case the forall there isn't actually 
needed so I just remove it.

> This is the main change
>
>>  restrictSubpaths :: (RepoPatch p) => Repository p C(r u t) -> [SubPath]
>> -                 -> IO (forall t m. FilterTree t m => t m -> t m)
>> +                 -> IO (TreeFilter m)
>
> and a particular example of the change in action.
>
> I'm guessing here we actually never needed that inner forall m in the
> first place and were only using impredicativity for t.

Correct. (I guessed that too and the type checker confirmed it for me :-)

Ganesh

On Wed, Jun 30, 2010 at 20:57:04 +0100, Ganesh Sittampalam wrote:
> >> type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y))
> >>-subcommutes :: [(String, CommuteFunction)]
> >>+subcommutes :: [(String, (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y)))]

> No, it is necessary :-) CommuteFunction has an explicit forall -
> it's just a type alias and those get expanded at each use site, so
> the old code had a forall inside the tuple type.

Whoops! :-)

> In other words a pair is something that takes two type variables as
> type parameters. As you say in the rest of your review,
> impredicativity makes it legal to instantiate those variables with
> types that have a top-level forall. Without impredicativity, that
> isn't legal so we have to change it somehow. It turns out that in
> this case the forall there isn't actually needed so I just remove
> it.

All clear.  Thanks for confirming away the shakiness too.

-- 
Eric Kow <http://www.nltg.brighton.ac.uk/home/Eric.Kow>
PGP Key ID: 08AC04F9

This patch bundle (with 1 patches) was just applied to the repository http://darcs.net/reviewed.
This message was brought to you by DarcsWatch
http://darcswatch.nomeata.de/repo_http:__darcs.net_reviewed.html#bundle-0c50e7f2922fb37df4e6e671bf8974abb3b9695c