[darcs-devel] The problem with repo witnesses
Ganesh Sittampalam
ganesh at earth.li
Sun Oct 22 16:05:37 UTC 2017
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.
> 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.
> 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.
Ganesh
More information about the darcs-devel
mailing list