On Sun, 30 Aug 2009, Jason Dagit wrote:
On Sun, Aug 30, 2009 at 4:06 PM, Ganesh Sittampalam<[email protected]> wrote:
On Sun, 30 Aug 2009, Jason Dagit wrote:
+invertQ :: (Invert p) => (FORALL(x y) p C(x y)) -> (FORALL(x y) p C(x y))
+invertQ p = invert p
I thought invert caused the context types to swap. So I would expect
this to be:
+invertQ :: (Invert p) => (FORALL(x y) p C(x y)) -> (FORALL(x y) p C(y x))
Well, it does type check :-) The trick is in the quantification; it gets
passed an unconstrained p and it gives back an unconstrained p, so it works
fine. To put it another way, we promise to provide p C(x y) for any x and y;
if the user of the result asks for p C(a b), then we'll ask the argument for
p C(b a), which it will happily provide since it also promises to provide a
p with any parameters.
Right, the foralls on both sides makes it very eager to unify. I just
find it odd that inverting doesn't change ordering of the contexts.
May I ask that the input context variables be different than the
output ones? For example:
+invertQ :: (Invert p) => (FORALL(x y) p C(x y)) -> (FORALL(a b) p C(a b))
This way people reading the code will automatically see they are not linked.
OK, will do.
+newtype Witnessed t C(x) = Witnessed { unWitnessed :: t }
This type is potentially very abusable. In the past David has asked
that I not create types like this. The data constructor is inherently
unsafe in the presence of unsafeCoerceP.
I don't follow what's unsafe about this. The contained value doesn't use the
x parameter, so it doesn't increase the extent to which you can coerce
between non-phantom types.
[...]
At one point during refactoring I introduced a type much like your
Witnessed type and then accidentally implemented unsafeCoerce by using
it. For this reason, I don't feel that it is an entirely theoretical
problem.
OK, I hadn't realised or had forgotten quite how bad the situation is.
In fact you can trivially implement unsafeCoerce just using is_identity
from Darcs.Patch.Prim (amongst many other such examples), so my feeling is
that this is a horse that has long since bolted.
I guess in one sense there is a problem in that unsafeCoerceP doesn't have a
constraint on the type constructor, so you can (ab)use it to coerce type
parameters that aren't actually phantom. Perhaps we should add a class to
restrict it to just those types that have two phantom parameters?
I discussed this in a private email with David (and perhaps Ian) while
working on this before. We came to the conclusion that doing so makes
it hard to work with patches and sequences of patches.
If I recall the best idea we had was something like:
data FL a x y where
NilFL :: (Context x, Context y) => a -> FL a x y
(:>:) :: (Context x, Context y, Context z) => a -> FL a x y -> FL a y z
Well, you could make the name of the class really short. Also in FL you
only absolutely need it on the existential type, not every single type;
though you will need it at many/most use sites too.
Then the Context type class would be something like this:
class Hidden a where
class Hidden a => Context a where
And then we can export the class Context but not the class Hidden and
use that mechanism to forbid making instances of Context.
As you can see this is going to add a lot of noise. So we decided it
was too much effort for little gain.
I guess there's a trade-off, but Haskell is fundamentally a safe language
and I'd quite like to have the darcs codebase also be safe ;-)
Hopefully my objects seem more reasonable now?
Yes, I now see what you mean, but I'm not convinced that Witnessed makes
the situation any worse than it already is.
Ganesh
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
