On Sun, Aug 30, 2009 at 4:06 PM, Ganesh Sittampalam<[email protected]> wrote:
> On Sun, 30 Aug 2009, Jason Dagit wrote:
>
>> On Sun, Aug 30, 2009 at 5:39 AM, Ganesh Sittampalam<[email protected]>
>> wrote:
>>>
>>> I'm not 100% sure that the witnesses patch is a good idea, so would
>>> appreciate
>>> comment/discussion.
>>>
>>> Mon Aug 3 06:19:07 BST 2009 Ganesh Sittampalam <[email protected]>
>>> * remove unused export
>>>
>>> Mon Aug 3 06:24:57 BST 2009 Ganesh Sittampalam <[email protected]>
>>> * add type witnesses to Darcs.Diff
>>>
>>> This doesn't affect the internal safety at all, in the same way that
>>> construction of primitive patches is not safe. However together with the
>>> introduction of "witnessed slurpies" it does enable a "safe" interface
>>> to be
>>> exported.
>>
>> I'm a natural person to look at this so I'm giving my thoughts/feedback.
>>
>> It's similar in spirit to the RIO stuff that I still need to finish.
>> Therefore, I see it as a good thing.
>>
>> I'm looking at this type and wondering how it works:
>> diff_at_path :: (Bool, Bool, Bool) -> (FilePath -> FileType)
>> - -> Slurpy -> Slurpy -> FilePath -> Maybe (FL Prim)
>> + -> Slurpy -> Slurpy -> FilePath -> Maybe (FL Prim C(y
>> z) -> FL Prim C(x z))
>>
>> How does it return a function that makes the sequence go from y to z
>> to x to z? Is it going to add or remove patches from the head of the
>> list? I would have guessed the type to be more like Maybe (FL Prim
>> C(x y) -> FL Prim C(x z)).
>
> Yes, it adds things to the head. Most of the code uses diff lists to avoid
> the quadratic slowdown from repeated use of (++) or equivalent, and adding
> things to the head is precisely how diff lists work.
Cool. I learned something new :)
>> +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.
>> +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.
I thought that for a long time as well. Looking in my thesis I see
this example, in Section 5.2.2 Unsound Equality Examples:
http://files.codersbase.com/thesis.pdf
-- Sorry if things don't line up perfectly
-- I typed it in a proportional width font
unsafeCoerce :: forall a b. a -> b
unsafeCoerce x = case a =\/= b of
IsEq -> x
_ -> error "a = b, making this impossible"
where (a, b) = (P, P) :: (P () a, P () b)
This assumes we have some data type:
data P a b = P
instance PatchEq P where
P =\/= P = unsafeCoerceP IsEq
P =/\= P = unsafeCoerceP IsEq
I give 2-3 other examples in that section, but the one here is the shortest.
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.
> Even if that wasn't the case I'd hope that uses of unsafeCoerceP would be
> audited to verify that they didn't do anything evil anyway.
Explicit calls to unsafeCoerceP are easy to spot, but the EqCheck type
witness exports a constrained form of unsafeCoerceP. The indirect
usages are the hard ones to spot. By introducing the witnessed type
we are increasing the number of 'unsafe' functions that we need to
audit for. In this case, the unsafe function is the data constructor.
Exporting something safe instead of the witnessed constructor is one
way to reduce the problem.
> 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
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.
Hopefully my objects seem more reasonable now?
Jason
_______________________________________________
darcs-users mailing list
[email protected]
http://lists.osuosl.org/mailman/listinfo/darcs-users
