[darcs-devel] The problem with repo witnesses

Ben Franksen ben.franksen at online.de
Thu Oct 26 19:31:32 UTC 2017


Am 22.10.2017 um 18:05 schrieb Ganesh Sittampalam:
> On 29/09/2017 21:07, Benjamin Franksen wrote:
>> We have a number of procedures that take a repo and return another one,
>> where we return the same repo, only with properly casted (coerced)
>> witness types. For instance
>>
>> tentativelyRemovePatches
>>   :: Repository rt p wR wU wT
>>   -> ...
>>   -> FL (PatchInfoAnd rt p) wX wT
>>   -> IO (Repository rt p wR wU wX)
>>
>> User code then looks like
>>
>>   repo' <- tentativelyRemovePatches ... repo
>>   repo'' <- ...more of the same using repo'...
>>   ...etc...
>>
>> This is ugly and repetitive; a common difficulty when threading state
>> manually. The standard solution is 'StateT s IO', but we cannot use it!
>> We do not have a single type for the state but a family, indexed over
>> symbols for the recorded, unrecorded, and tentative repo state. We would
>> need an indexed version of StateT.
> 
> It's also unsafe, as you might accidentally re-use an older version of
> 'repo'. There's some chance that linear types will be added to GHC soon:
> https://www.tweag.io/posts/2017-03-13-linear-types.html, which might be
> nice to experiment with.

Ha! Thanks for the link, that's interesting. It's quite a big hammer,
though.

>> There is the "indexed" package, which we could use. Our procedure would
>> get this type:
>>
>> tentativelyRemovePatches
>>   :: ...
>>   -> FL (PatchInfoAnd rt p) wX wT
>>   -> IxStateT IO (Repository rt p wR wU wT) (Repository rt p wR wU wX) ()
>>
>> [IxStateT is from indexed-extra, in case you are wondering]
>>
>> [The name 'Repository' is too long for that kind of stuff, need an
>> abbreviation]
>>
>> I haven't tried yet if this actually works.
> 
> I've been interested in finding a better way to handle this for a while.
> I think we'd probably be best off writing our indexed monad type as then
> we wouldn't need to include 'Repository rt p' in type signatures twice,
> though we could also use a type alias. The biggest annoyance is either
> having to give up do-notation or to play with some of the
> NoImplicitPrelude tricks, which tend to either mean you can't use
> do-notation on normal IO, or you need some type class that makes type
> inference worse.

Yes, yes, yes.

>> Another problem is that the RepoJob machinery requires that the job
>> procedure is parametric in some of the witnesses. The job must have type
>>
>>   forall wR wU... Repository rt p wR wU wR -> ...
>>
>> and for most commands this is the correct type: the job should be able
>> to handle any recorded or unrecorded state and the tentative state is
>> the same as the recorded one, since we just started a transaction (or
>> the command is read-only). But for some it is too restrictive, e.g.
>> convert and clone both work on a freshly created repo and thus do not
>> fit this scheme, which means we must coerce the type, which means we
>> could have spared ourselves the trouble of giving precise types to
>> repos. But neither do I like the idea of adding yet another variant to
>> the RepoJob type. Not sure what to do.
> 
> Commands that require there to be no unrecorded changes but where there
> might be some anyway typically do a 'readUnrecordedChanges' and
> pattern-match on the result to prove wR ~ wU. Perhaps operations that
> create a repository could return a witness that 'wR ~ wU' instead.

Doing readUnrecordedChanges (or readRepo for that matter) and pattern
matching on the result is a run-time check. When you operate on some
arbitrary repo that's okay, you'd need the run-time test anyway. But
it's ridiculous to do that with a repo we just created: we statically
know this thing has no recorded changes, no unrecorded changes, no
rebase in progress etc.

My conclusion is that using RepoJob for newly created repos makes no
sense. Instead createRepository should return a properly typed
Repository which we can use directly in a command without further ado. I
am in the last stages of preparing (actually testing) a patch that does
this and I think it's a definite improvement.

Cheers
Ben



More information about the darcs-devel mailing list