[darcs-users] [patch40] stop using impredicativity

[Eric Kow]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 195 bytes
Desc: not available
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20100630/02b69388/attachment-0001.pgp>