[darcs-devel] [patch1807] drop our custom EqCheck type for (:~:) from base

Ganesh Sittampalam bugs at darcs.net
Thu Aug 8 22:35:35 UTC 2019


Ganesh Sittampalam <ganesh at earth.li> added the comment:

On 08/08/2019 17:55, Ben Franksen wrote:

>> patch 2ad67fe045d12c1574a1003cb93fc469f7b0344b
>> Author: Ganesh Sittampalam <ganesh at earth.li>
>> Date:   Tue Aug  6 18:50:09 CEST 2019
>>   * drop our custom EqCheck type for (:~:) from base
> 
> I am not convinced we should replace EqCheck wX wY with Maybe (wX :~:
> wY) everywhere. This is more noisy and harder to type, due to the infix
> operator and the parens. I also find "IsEq" easier to read and more
> intuitive than "Just Refl". We could define EqCheck as a type synonym,
> but that doesn't give us back NotEq and IsEq.

Yep, fair enough.

It now occurs to me that maybe something nicer could be done with
pattern synonyms. I'll have a play with that.

>
>> patch 261ac89aa2af3586d1dd6851a7cf47adc94d8305
>> Author: Ganesh Sittampalam <ganesh at earth.li>
>> Date:   Tue Aug  6 21:48:48 CEST 2019
>>   * Give patch contexts their own kind
> 
> In principle the idea of defining a special kind for witnesses sounds
> right to me. But I think this needs more thought to design in a way that
> better captures the mathematical meaning of witnesses.
> 
> In my view a witness symbolically represents a /set/ of repository
> states i.e. the domain or range of the partial bijection represented by
> the patch or patch sequence. Neither the name nor the constructors of
> 'PatchContext' express this very well.

Agreed, but isn't it still better than the current situation? Or is the
extra overhead only justified if we do better than the current proposal?
 I think even if we were going to go the whole way, this patch would be
a good stepping stone as it deals with the annoying kind signatures
bookkeeping.

> The fact that the 'Add'
> constructor is not used anywhere to construct witnesses is a hint that
> something doesn't fit here.
Yes - our witnesses do at least now live in the right universe, but we
haven't structured the universe correctly or made any attempt to use its
structure.

It may be worth having a go at using type level sets to model this
properly. I had a little bit of an attempt years ago when we first added
witnesses, but it was totally beyond the reach of the Haskell type
system then. Now I think it's at least plausible, and I've successfully
used the 'type-level-sets' package on Hackage in some other,
smaller-scale, code. But I would guess it'd still be a significant effort.

> Even 'Origin' is not unproblematic.

> The name 'Origin' suggests that this is a specific state, one without
> patches i.e. an empty repo. This is quite fitting for PatchSets, since
> their representation as an RL of tagged sections i.e. inventories
> requires that. But when we take the sequence of all patches in a
> PatchSet, then we can perfectly well apply this to a non-empty state (as
> long as it is suitably disjoint).

I don't get this point. It's no different from taking a sequence from
one context and applying it to another; you have to commute, or coerce
the witnesses. If your PatchSet started from Origin, the sequence you
get from it does too.

> The truth is that using 'Origin' allows us to treat a PatchSet as if it
> had only one witness i.e. as if its left witness were existentially
> quantified, without actually defining it in this way. Because for
> technical reasons we want PatchSet to have the same kind as a patch (so
> we can put it into a Fork, :>, :\/: etc).

I guess it makes sense that PatchSet would normally be used with a
starting context of 'Origin', as that's what makes its clean tag
invariants valid and establishes the connection to the on-disk format.

But regardless of whether we use Origin for PatchSet explicitly or
implicitly, I don't see that the left witness should be existentially
quantified. An empty repo is a known state, not an unknown one.

Aside: I had a quick go at changing the constructor of PatchSet to
change wStart to Origin. It looks like that would actually be feasible:
there's one place in Rebase that constructs a patch set from the rebased
patches just to pass to the existing log code, but other than that all
the types went through without coercion.

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/patch1807>
__________________________________


More information about the darcs-devel mailing list