[darcs-users] [patch40] stop using impredicativity

Eric Kow kowey at darcs.net
Wed Jun 30 17:18:46 UTC 2010

On Sat, Jun 26, 2010 at 16:35:22 +0000, Ganesh Sittampalam wrote:
> Sat Jun 26 17:30:16 BST 2010  Ganesh Sittampalam <ganesh at 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 198 bytes
Desc: Digital signature
URL: <http://lists.osuosl.org/pipermail/darcs-users/attachments/20100630/33d9001d/attachment.pgp>

More information about the darcs-users mailing list