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

[Ganesh Sittampalam]

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

On 09/08/2019 09:50, Ben Franksen wrote:

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

Fair enough. Thinking about it a bit more, we might actually be able to
use PolyKinds to get better inference, I'll have a play. But even with
that it might still be too much overhead, I'm not particularly desperate
to introduce this.

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

I'm not sure it's that complicated. What I had in mind was:

 - define a kind representing patches
 - define contexts as a set of patches

Interesting questions would be:
 - what we would actually use to represent patches at the type-level.
Perhaps just a Symbol. As with the current patch, there wouldn't be any
concrete instantations except in the test harness.
 - the level of granularity for a single patch - would it be a prim, or
something else?
 - how to deal with inverses. In most cases they would need to remove a
patch from a set, which would complicate things.

Overall I agree it's likely that it'll still be too hard, or too
expensive in compile time or maintenance time. The gain would be that we
could give a proper type to commute and merge, but it's not all that
compelling either.

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

I still don't get it. The darcs code is all about manipulating
*representations* of patches, which always apply in a specific context.
If you want to apply a patch sequence in a different context, you have
to commute it explicitly, even if that's a trivial operation.

If we reflected some mathematical structure in our witnesses, we could
give richer types to operations like commute, but we still wouldn't be
able to take a patch representation and freely apply it in any other
context.

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