[darcs-users] repository IO and type witnesses

[Ganesh Sittampalam]

Hi David,

As Jason mentioned, I've been trying to help Jason sort out some of the 
repository type witness stuff. I've been getting rather confused by the 
discussions you've been having, perhaps I only have a high level view of 
things. However I'm not convinced that the types you are proposing make 
complete sense, so I'd like to propose an alternative, and thus clear up my 
confusion one way or another.

As I understand it, the current plan is to have

newtype RIO p C(r u t t') a = UnsafeRIO (Repository p C(r u t) -> IO a)

The idea being that an action of type RIO p C(r u t t') a operates on a 
repository that contains patches of type p, and that is in recorded state r, 
unrecorded state u, and tentative state t, and returns one in tentative state 
t' (other states unchanged).

With this type, RIO covers all the tentative operations. For other operations, 
the changing states are handled by a changing Repository, for example your 
proposed withGuts:

> withGutsOf :: Repository p C(r u r) -> RIO p C(r u r t)
>           -> IO (Repository p C(t u t)

The problem I see with returning a Repository value, and indeed having type 
witnesses for repository states in the Repository type, is that they are being 
treated like normal functional values, when in fact they are just a handle to 
a single-threaded thing, namely what's actually on disk right now. In that 
sense they are like IORefs or STRefs, rather than the state in a normal state 
monad, which you can grab hold and keep an old copy of while writing a new 
state into the monad.

So the RIO type properly models this single-threadedness for the tentative 
state, but not for the recorded or unrecorded state. It was the intuition 
that any of these states could change that was behind the original 
suggestion Jason mentioned that RIO should take two parameters of type 
(RepoInState r u t) - the RepoInState type just serving to cut down the 
number of direct parameters to RIO. Repository should just be Repository p 
- the actual state it's in would be determined by the current RIO type 
parameters.

The way I see this approach working is that the RIO type would bubble all 
the way up through into Darcs.Commands.*, and only at the highest possible 
level in that would it be "lowered" back into IO.

So, in this world, we would have

data RepoInState r u t
data Repository p = ...
newtype RIO p s s' a = UnsafeRIO (Repository p -> IO a)

and then all the tentatively* code would have return types like

RIO p (RepoInState r u t) (RepoInState r u t') a

whereas for example a command like record -a would be (perhaps this is a bit 
too simple, but you get the idea)

RIO p (RepoInState r u r) (RepoInState u u u) a

Does this make some kind of sense, or have I completely misunderstood the 
goals of the witness addition? To me, this seems like the right long-term 
place to be, even if the short term goals are only to add safety to a 
subset of the repository affecting code - but in that case getting the 
types right from the beginning would still make sense.

Cheers,

Ganesh