[darcs-devel] (un)safety of unsafeCompare

Ganesh Sittampalam ganesh at earth.li
Sat Jul 6 16:23:17 UTC 2019


Hi Ben,

I think what you say about "better make sure that all the other
operations are consistent with that definition" is exactly what I am
thinking of when I say "proof obligation".

If you do violate that proof obligation, so that supposedly equal
patches don't produce the same result when applied, then you end up
being able to do the exact equivalent of 'apply (unsafeCoerceP x)'.

I don't think we disagree about what code would be correct and what
wouldn't, so the question is just how to communicate that to others. I
don't feel too strongly about exactly how we do that.

Cheers,

Ganesh

On 06/07/2019 16:47, Ben Franksen wrote:
> Hi Ganesh
> 
> I think I begin to understand why we see this differently.
> 
> My point of view is that an instance of class Eq2 /defines/ what
> semantic equality means for that patch type. As long as the equality
> thus defined is an equivalence relation, coercing the witnesses as done
> by the default method implementations for =\/= and =/\= is correct by
> definition. Indeed, if I write
> 
>   unsafeCompare _ _ = True
> 
> then I am stating that all patches are considered equal. Coercing
> opposing witnesses is therefore completely justified and does not in any
> way compromise the witness system!
> 
> Of course, if I make such a definition I'd better make sure that all the
> other operations are consistent with that definition. That is, when I
> apply such a patch I should get the same result for all patches etc. But
> this is not different to defining instances of the good old Eq for
> unwitnessed types: if == should mean semantic equality then you better
> make sure that any function f respects equality in the sense that x == y
> ==> f x == f y.
> 
> In contrast, calling unsafeCoerce really is /undefined/ in the same
> sense that calling 'apply (unsafeCoerceP x)' is undefined, in general,
> unless you can prove that your contexts are actually equivalent. I could
> think of patch types that contain a runtime representation of the start
> and end states and IMO it would be fully justified to call error
> 
> Cheers
> Ben
> 
> Am 05.07.19 um 17:58 schrieb Ganesh Sittampalam:
>> On 30/06/2019 01:07, Ben Franksen wrote:
>>> The haddocks for class Eq2 say the following about unsafeCompare:
>>>
>>>> It is unsafe to define a class instance via this method, because if
>>>> it returns True then the default implementations of '=\/=' and '=/\='
>>>> will coerce the equality of two witnesses.
>>
>> I think here that "unsafe" means "you have a proof obligation". For
>> example if I wrote
>>
>>   unsafeCompare _ _ = True
>>
>> then a caller could use =\/= to equate two unequal contexts.
>>
>> Conversely defining the class with =\/= and not using unsafeCoerce in
>> the implementation, can't introduce any extra unsafety. Clearly such an
>> implementation would ultimately need to delegate to something that is
>> "unsafe" (in the above sense).
>>
>>>> Calling this method is safe, although '=\/=' or '=/\=' would be
>>>> better choices as it is not usually meaningul to compare two patches
>>>> that don't share either a starting or an ending context
>>> I think this statement gets it wrong. In fact the opposite is true.
>>>
>>> It is unsafe to /use/ unsafeCompare because this may mean that we
>>> identify two patches that may only accidentally have the same structure,
>>> but are otherwise completely unrelated. Here is a simple example:
>>>
>>>   A=hunk f [x] [y]; B=move f g; C=add f; D=hunk f [x] [y]
>>>
>>> For these patches,
>>>
>>>   unsafeCompare A D = True
>>>
>>> even though A and D are decidedly /not/ the same patch!
>>
>> That's true, but we also don't get any equality coercion we can then misuse.
>>
>> So I think the existing comment is correct in the narrow sense that
>> defining unsafeCompare imposes a proof obligation that the patches
>> genuinely are equal. That means that when called with equal starting
>> contexts, it's safe to coerce the ending contexts. Complying with that
>> (informal) proof obligation in turn means that the safety of the witness
>> system is preserved.
>>
>> Calling unsafeCompare is probably never/almost never actually the right
>> thing to do, but it doesn't in itself compromise the witness system.
>>
>> I guess this particular comment could be improved to give more details
>> of that. In general the meaning of "unsafe" in the codebase is probably
>> not clearly nailed down and some general documentation of that might be
>> helpful.
>> Cheers,
>>
>> Ganesh
>>
> 
> 
> _______________________________________________
> darcs-devel mailing list
> darcs-devel at osuosl.org
> https://lists.osuosl.org/mailman/listinfo/darcs-devel
> 



More information about the darcs-devel mailing list