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
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users

Reply via email to