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

Ben Franksen bugs at darcs.net
Fri Aug 9 08:50:31 UTC 2019


Ben Franksen <ben.franksen at online.de> added the comment:

>>>   * 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?

The current situation may not be perfect but it strikes a nice balance
between reasonably low overhead and a huge benefit wrt safety and
additional structure. I like it very much that GHC can infer the kind of
patch type variables. Giving that up IMO requires a justification that
is stronger than guarding against the near zero chance that someone
mistakenly abuses unsafeCoerceP to cast between regular types.

> 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.

This is correct. And I'd be willing to sacrifice some convenience if we
had a clear picture of the goal and we knew it was only a matter of hard
work to reach it. This is not the case, though. The end goal remains
quite elusive and I am far from convinced it it is reachable at all, in
practice, even with some future "full spectrum dependent" Haskell.

>> 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.

Keep in mind that the sets we talk about are all infinite subsets of an
infinite state space. I have a hard time imagining a model of that in
Haskell's type/kind system. Even assuming you get this done, compile
times may well go through the roof as a result. And the proofs must all
be done manually, without tactics and proof scripts as in Coq. Any
change to the code will require a manual re-write of the proofs (aka
type signatures).

Despite these misgivings, it may still be worthwhile to pursue this
goal. Perhaps we find some clever trick to express the additional
structure we want efficiently. But until I see a clear picture of where
this leads to, so I can judge the benefits it will give, I am unwilling
to make preparatory steps toward it in our code base.
>> 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.

You are right. This is an inherent weakness of our current witness
system and not particular to Origin.

We can express that patch sequences form a groupoid, but we cannot
(yet?) express that this is an /inductive/ groupoid. For that we would
need a lattice order on our witnesses i.e. this is the sort of "end
goal" we may want to reach one day with a dedicated kind for witnesses.

>> 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.

Yes, I concede that point.

> 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.
Yes, this is something I often wondered about. If you have already made
this change, please send a patch. This sounds like a good move. But I
think there is one place (related to patch bundles or context files)
where we actually use a PatchSet that does not start at the Origin. This
always felt like an ugly hack to me, though, and I am all for cleaning
that up.

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


More information about the darcs-devel mailing list