Just for discussion for now. I've replaced EqCheck wA wB
with Maybe (wA :~: wB).

It's always nice not to roll our own for standard concepts,
and it means we can occasionally use (wA :~: wB) directly.

On the other hand the change will probably conflict with
other WIP, and it does make things a bit more verbose -
e.g. Just Refl is longer than IsEq.

1 patch for repository darcs-unstable@darcs.net:screened:

patch 8a9b8365cb739b10bc1b282109da85a55e78c3a2
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun Jun  9 10:52:37 BST 2019
  * drop our custom EqCheck type for (:~:) from base

Attachments

• drop-our-custom-eqcheck-type-for-_____-from-base.dpatch
• patch-preview.txt
• unnamed

Updated bundle with more possible updates to witnesses etc.

I'm not sure any of them except dropping Darcs.Patch.Type
is that compelling. The 'role nominal' one isn't very
invasive and adds a bit of safety, so is probably worth it
as well.

4 patches for repository darcs-unstable@darcs.net:screened:

patch 8a9b8365cb739b10bc1b282109da85a55e78c3a2
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun Jun  9 10:52:37 BST 2019
  * drop our custom EqCheck type for (:~:) from base

patch c1f343cadad9a2f1ba9fdaa1cc8fb1226d1cbc08
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 07:06:02 BST 2019
  * make sure patch context witnesses have role nominal
  
  This makes sure calling code can't use coerce to change the
  witnesses.
  
  We only need to do this for the low-level types. Higher-level
  ones that take other patches as parameters will have this role
  inferred anyway.

patch 34588de518a656932affad4fa33556612b8e47a7
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 07:37:58 BST 2019
  * Give patch contexts their own kind

patch 4b92c674ba371121fe71234b349a01989ba21e78
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 08:08:05 BST 2019
  * drop Darcs.Patch.Type and use TypeApplications instead

Attachments

• drop-our-custom-eqcheck-type-for-_____-from-base.dpatch
• patch-preview.txt
• unnamed

> Just for discussion for now. I've replaced EqCheck wA wB
> with Maybe (wA :~: wB).
> 
> It's always nice not to roll our own for standard concepts,
> and it means we can occasionally use (wA :~: wB) directly.
> 
> On the other hand the change will probably conflict with
> other WIP, and it does make things a bit more verbose -
> e.g. Just Refl is longer than IsEq.

I like the idea though I haven't been looking at the changes in details
yet. Your comment about conflicts with WIP is appreciated, indeed I
would like you to postpone this until we get V3 in screened. I think I
need to make a bundle for that sooner rather than later.

> Updated bundle with more possible updates to witnesses etc.
> 
> I'm not sure any of them except dropping Darcs.Patch.Type
> is that compelling.

Yes, this one strikes me as a nice way to make use of type application.
I am also fine with using it in the test harness, instead of passing
undefined :: Whatever.

> The 'role nominal' one isn't very
> invasive and adds a bit of safety, so is probably worth it
> as well.

Agreed.

Darcs.Patch.Witnesses.Kind looks interesting but it could use a bit of
documentation. I don't quite grok what's going on there...

It is a bit unfortunate that this bundle has so many conflicts with
screened now. (Sorry about that.) I guess it makes sense to rebase your
patches and resend, makes it a bit easier to apply and the view in a
side-by-side diff. (For now I helped myself with a 'darcs rebase apply'
in a separate clone.)

Updated version of the patches. I've added some documentation
to the patch kind type.

Let's make a decision either way on these soon as they'll rot
quite fast (especially the last two). I think we should at
least take the first two.

We can also migrate from all the undefineds over the test
harness to type applications, but that might as well go in
separate patch(es).

4 patches for repository darcs-unstable@darcs.net:screened:

patch c66ef0ecf7a1e57c3eaf2cc74e8abb402d8bcdac
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Aug  6 16:57:59 BST 2019
  * drop Darcs.Patch.Type and use TypeApplications instead

patch c1f343cadad9a2f1ba9fdaa1cc8fb1226d1cbc08
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Jun 11 07:06:02 BST 2019
  * make sure patch context witnesses have role nominal
  
  This makes sure calling code can't use coerce to change the
  witnesses.
  
  We only need to do this for the low-level types. Higher-level
  ones that take other patches as parameters will have this role
  inferred anyway.

patch 2ad67fe045d12c1574a1003cb93fc469f7b0344b
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Aug  6 17:50:09 BST 2019
  * drop our custom EqCheck type for (:~:) from base

patch 261ac89aa2af3586d1dd6851a7cf47adc94d8305
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Tue Aug  6 20:48:48 BST 2019
  * Give patch contexts their own kind

Attachments

• drop-darcs_patch_type-and-use-typeapplications-instead.dpatch
• patch-preview.txt
• unnamed

> patch c66ef0ecf7a1e57c3eaf2cc74e8abb402d8bcdac
> Author: Ganesh Sittampalam <ganesh@earth.li>
> Date:   Tue Aug  6 17:57:59 CEST 2019
>   * drop Darcs.Patch.Type and use TypeApplications instead
> 
> patch c1f343cadad9a2f1ba9fdaa1cc8fb1226d1cbc08
> Author: Ganesh Sittampalam <ganesh@earth.li>
> Date:   Tue Jun 11 08:06:02 CEST 2019
>   * make sure patch context witnesses have role nominal
>   
>   This makes sure calling code can't use coerce to change the
>   witnesses.
>   
>   We only need to do this for the low-level types. Higher-level
>   ones that take other patches as parameters will have this role
>   inferred anyway.

These first two patches are perfectly fine.

> patch 2ad67fe045d12c1574a1003cb93fc469f7b0344b
> Author: Ganesh Sittampalam <ganesh@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.

> patch 261ac89aa2af3586d1dd6851a7cf47adc94d8305
> Author: Ganesh Sittampalam <ganesh@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. The fact that the 'Add'
constructor is not used anywhere to construct witnesses is a hint that
something doesn't fit here. 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).

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

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

>> patch 2ad67fe045d12c1574a1003cb93fc469f7b0344b
>> Author: Ganesh Sittampalam <ganesh@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@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.

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

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.

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

I thought so, too, but my (short, few) experiments weren't successful.

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

Ah, this is quite different from what I had in mind. This "internal"
definition of contex indeed corresponds quite closely to how our
witnesses work. But as such it makes much more fine-grained distinctions
between contexts than would be necessary: there are many different
"contexts" that map via the apply functor to the same set of states. It
is this set of states that I regard as the "real" definition of context.

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

(If all patches had either an explicit identity or at least a canonical
representation, we could hash that and use as a type-level number.)

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

Interesting. What do you think is wrong about the types of commute and
merge?

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

We need to agree on a precise definition of context, otherwise this
discussion makes no sense and we won't understand each other.

My understanding is that a patch sequence represents a partial bijection
between ApplyStates (say Trees). The context of a patch p is the domain
of that bijection: the set of all ApplyStates for which 'apply p' is
defined.

> 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 that is a trivial operation, then why do I have to perform it?

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

In my definition it would be the /same/ context /by definition/.

On 09/08/2019 15:13, Ben Franksen wrote:

>>  - 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.
> 
> (If all patches had either an explicit identity or at least a canonical
> representation, we could hash that and use as a type-level number.)

Remember this is all in the static types. We don't have a concrete patch
at compile-time, so we can't actually construct a specific type-level
number at compile-time. All we will actually have are type variables,
perhaps existentially quantified.

>>  - 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.
> 
> Interesting. What do you think is wrong about the types of commute and
> merge?

Just that the result type is existentially quantified. We know more than
that: if we do the same commute or same merge twice we get the same new
context, and if we reverse a commute or a merge using the laws, we get
back to the original context.

Not sure if we ever run across this in practice. Perhaps in the
implementation of things like taggedIntersection/findCommonAndUncommon.

>>> 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.
> 
> We need to agree on a precise definition of context, otherwise this
> discussion makes no sense and we won't understand each other.
> 
> My understanding is that a patch sequence represents a partial bijection
> between ApplyStates (say Trees). The context of a patch p is the domain
> of that bijection: the set of all ApplyStates for which 'apply p' is
> defined.

Here's my understanding:

A single patch/patch sequence value in memory should only ever be
applied to one specific Tree. This reflects the way darcs behaves: if
you want to apply a specific patch representation, you have to have to
do so on top of the precise set of patches it was constructed for. If
you want to apply it to any other set of patches, you have to commute first.

So given 'p wX wY', the context 'wX' is a proxy for a specific set of
patches. In turn that set of patches implies one specific Tree.

IMO the fact that darcs keeps careful track of one specific correct
context for a patch representation is fundamental and part of what sets
it apart from just keeping a set of diffs. The safety that witnesses
gives us isn't just about making sure that a patch will apply cleanly
when we come to do it, but also that we don't accidentally use it in a
superficially valid but actually wrong 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 that is a trivial operation, then why do I have to perform it?

Because it might not be trivial. Commuting a hunk change to file A and
one to file B is trivial, commuting two hunk changes to file A aren't.

>>>  - 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.
>>
>> (If all patches had either an explicit identity or at least a canonical
>> representation, we could hash that and use as a type-level number.)
> 
> Remember this is all in the static types. We don't have a concrete patch
> at compile-time, so we can't actually construct a specific type-level
> number at compile-time. All we will actually have are type variables,
> perhaps existentially quantified.

Ah, yes, right. This is only possible with full spectrum dependent types.

>> What do you think is wrong about the types of commute and merge?
> 
> Just that the result type is existentially quantified. We know more than
> that: if we do the same commute or same merge twice we get the same new
> context, and if we reverse a commute or a merge using the laws, we get
> back to the original context.

Okay, understood. We don't know the intermediate context when we commute
patches but we know it satisfies some properties related to the original
context. Similar for merge. The idea was to express this kind of
knowledge in the types.

> Not sure if we ever run across this in practice.

We certainly do. I have stumbled over such cases, wondering why in hell
we need an unsafeCoerceP here... some of them even carry comments that
explain why we need the coercion. Can't remember where exactly, though.

>>>> 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.
>>
>> We need to agree on a precise definition of context, otherwise this
>> discussion makes no sense and we won't understand each other.
>>
>> My understanding is that a patch sequence represents a partial bijection
>> between ApplyStates (say Trees). The context of a patch p is the domain
>> of that bijection: the set of all ApplyStates for which 'apply p' is
>> defined.
> 
> Here's my understanding:
> 
> A single patch/patch sequence value in memory should only ever be
> applied to one specific Tree. This reflects the way darcs behaves: if
> you want to apply a specific patch representation, you have to have to
> do so on top of the precise set of patches it was constructed for. If
> you want to apply it to any other set of patches, you have to commute first.

I agree that your definition is the one that factually describes what we
do in Darcs (with the exception of those cases where we use
unsafeCoerceP). But I am not satisfied with that. It doesn't capture
what we /could/ do, mathematically speaking. It is just an easy to
calculate approximation. In fact it is so easy to calculate that the
type checker can do it for us ;-)


> So given 'p wX wY', the context 'wX' is a proxy for a specific set of
> patches. In turn that set of patches implies one specific Tree.

Yes. But this limitation is not a necessary one, imposed by patch
theory. It is just

I just want to stress here that in principle a patch, even our concrete
representations of a patch, can be applied to an infinite number of
states, not just one. It is just hard to calculate that set. Even merely
calculating membership in that set, given a concrete patch, is hard.

> IMO the fact that darcs keeps careful track of one specific correct
> context for a patch representation is fundamental and part of what sets
> it apart from just keeping a set of diffs. The safety that witnesses
> gives us isn't just about making sure that a patch will apply cleanly
> when we come to do it, but also that we don't accidentally use it in a
> superficially valid but actually wrong context.

I agree! Our approximation is /conservative/ and rightly so. It is safe
in that is doesn't allow applying a patch to a wrong context. But at the
same time it prevents us from applying it to some good contexts.

This is always the problem with static typing: you forbid bad programs
but at the price of also forbidding some good programs. All the effort
that goes into making type systems, especially Haskell's, more powerful
are motivated by the desire to enlarge the set of of good programs that
type check while still disallowing any bad programs.

The only point I want to make is that this definition of context is
purely technical. It has no semantic meaning in the theory. In theory we
can apply a patch to an infinite number of states and if we are very
careful we can actally do it, using unsafeCoerceP. The proof obligation
amounts to showing that the states we apply the patch to are actually in
its domain.

In know this is not the complete story, explicit patch identities
complicate things, since we have to maintain additional invariants. But
for raw unnamed prim patches this is true beyond any doubt.

>>> 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 that is a trivial operation, then why do I have to perform it?
> 
> Because it might not be trivial. Commuting a hunk change to file A and
> one to file B is trivial, commuting two hunk changes to file A aren't.

Yes, exactly. We cannot /know/ all the states that a patch can be
applied in. So we limit ourselves, via witness types, to those states
that we /can/ know are safe. But this is and remains an approximation.
And occasionally, we, the programmers, know that and therefore use an
unsafe coercion.

Just a quick follow-up on the overhead-reducing ideas, neither of 
which work/are worth it.

PolyKinds for patch contexts doesn't help because much of the time 
it just flips things from having the wrong inferred kind to having
a too general kind which then doesn't work in contexts where that
kind needs to match exactly, e.g. instantiating a rank-2 parameter.

PatternSynonyms do work to turn EqCheck into a type synonym + 
patterns IsEq and NotEq. However, they can't be exported as if
they were constructors of EqCheck (because it's not a data 
constructor). So you end up having to import the patterns
explicitly. Also you can't unsafeCoerceP IsEq anymore, you have to 
write Just (unsafeCoerceP Refl).

It is possible to turn the existing EqCheck into a newtype around
Maybe :~:, and use pattern synonyms to recover the exact behaviour
of IsEq/NotEq including exporting and coercing it. But I don't
really see any advantages to doing so.

I've pushed the first two patches to screened btw.

Marking this as accepted for the first two patches, last two are 
rejected.