On Sat, Jun 26, 2010 at 16:35:22 +0000, Ganesh Sittampalam wrote: > Sat Jun 26 17:30:16 BST 2010 Ganesh Sittampalam <gan...@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
signature.asc
Description: Digital signature
_______________________________________________ darcs-users mailing list darcs-users@darcs.net http://lists.osuosl.org/mailman/listinfo/darcs-users
