Re: My current work on darcs...

Please disregard, I hit the send button prematurely.

On 09/27/2017 05:24 PM, Benjamin Franksen wrote:
> On 09/14/2017 10:28 AM, Ben Franksen wrote:
>> Like I said last time, whether we operate on the tentative or the "real"
>> recorded state should not be visible outside the Repository layer. Thus,
>> we should not distinguish between them in the witnesses for the
>> Repository type. Instead, we should add a witness for the pending state.
>> (The repo type parameter should be kept as long as we mix rebase and
>> normal patches.) This gives us
>>
>>   Repository rt p wR wP wU
>>
>> which should be understood to mean that when we read the complete repo
>> we get
>>
>>   (recorded :> pending :> working)
>>   :: PatchSet rt p Origin wR :> Pending p wR wP :> Working p wP wU
> 
> I have been playing on and off with this idea. One problem I encountered
> regularly is that when we have a function that returns a patch or a
> patch list in such a way that we know that the starting and ending
> states do not change, then it should be possible to avoid sealing:
> 
>   do_some_internal_commutation :: (FL p) wX wY -> (FL p) wX wY
> 
> But that fails to compile for the trivial case:
> 
>     do_some_internal_commutation NilFL = NilFL
> 
> with an error could not deduce wX ~ wY
>