[darcs-users] [patch40] stop using impredicativity
ganesh at earth.li
Wed Jun 30 19:57:04 UTC 2010
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
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 :-)
More information about the darcs-users