[darcs-users] darcs patch: Is this Monadish?

Jason Dagit dagit at codersbase.com
Thu Aug 28 20:37:17 UTC 2008


On Thu, Aug 28, 2008 at 11:22 AM, David Roundy <droundy at darcs.net> wrote:

> It seems to me that our real problem is that in order for type
> witnesses to ensure that IO operations on repositories are performed
> in a safe manner, and that means ensuring that correct code can
> compile.  Since correct code cannot possibly compile unless we include
> the proof that the initial tentative state is the same as the recorded
> state, this seems critical to me.  The fact that my withRepository
> type also ensures that we cannot modify a repository without taking a
> lock on it is also a Good Thing, but is considerably less critical.
>
> But perhaps there is some real problem that I'm not aware of?

Again, I wasn't disagreeing with the new type for withRepoLock.  Just
stating that I don't see how this solves the problems that come up
later down the road.  I don't understand it == I can't implement it.
If we can solve the LHS maybe I can find time for the RHS.

> there is no t' or t'' here, and there must not be.  The Monad only
> allows actions that don't change state.

I thought the point was for the Monad to allow actions that don't
*track* the state.  We are doing IO under the hood after all.  So it
seems like a lie to claim that we don't allow actions that change
state, since internally anything is still possible.

I still don't understand what is the difference between the derived
instance and the specified one above.  I do understand the types of
the instances.  The newtype deriving hasn't been a source of
confusion, at least not for me.  I pointed out in my original email
that it might be wrong for our type safety.  Clearly, the newtype
derived instance looks like this:

instance Monad (IORepo p i j) where
 (>>) :: IORepo p i j a -> IORepo p i j b -> IORepo p i j b

While you're saying we should have:
instance Monad (IORepo p i i) where
 (>>) :: IORepo p i i a -> IORepo p i i b -> IORepo p i i b

I'm saying, I don't understand why the second one is safer than the first.

Are you saying that the first one allows for IO actions that knowingly
change the repo state whereas the other one is safe because it only
allows IO actions that either unknowingly change the state or don't
change it at all?

It seems to me that return is more problematic than (>>) if your goal
is to disallow IO actions that might knowingly modify repository
state.    On the other hand, a custom io :: IO a -> IORepo p i i a,
helps to make this safer in practice (not theory) since most IO
actions get in there via io.

> See below about FlexibleInstances.

FlexibleInstances seem to be documented here:
http://haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#instance-rules

All that we're getting from FlexibleInstances is the ability to list
non-distinct type variables.  Okay, that doesn't sound so bad anymore.
 In our case, it's "InstancesWithEqualTypes"

>> The problem for me is that I don't see how to apply this approach.  I
>> thought we were trying to fix things like tentativelyMergePatches.
>> But, here we're now concerned with withGutsOf.
>
> withGutsOf brackets all the functions like tentativelyMergePatches.
> Or rather, it currently brackets all such cases that are dangerous on
> darcs-1 repositories (amend, obliterate, optimize --reorder).  I'm
> proposing that we could extend it to bracket all uses of tentative
> functions, which would enable us to move those functions into RIO,
> without touching the rest of the code.

So you're saying that I only have to modify functions which get
bracketed by withGutsOf?  That might not be so bad.

> We could easily leave both functions in place.  So we'd have
>
> unsafeTentativelyMergePatches :: ... -> IO (Sealed (FL Prim C(u)))
>
> and
>
> tentativelyMergePatches :: ... -> RIO (Sealed (FL Prim C(u)))
>
> and most likely tentativelyMergePatches would be implemented in using
> unsafeTentativelyMergePatches.
>
>> I don't have #1 for either approach which is a show stopper both for
>> type witnessing the commands and implementing RIO.
>
> Why is tentativelyMergePatches particularly problematic?

In your example you didn't put in the rest of RIO, and that's the part
I'm not understanding.

tentativelyMergePatches :: ... -> RIO p C( what goes here ?) (Sealed
(FL Prim C(u)))

One problem is that I suspect the final tentative recorded state for
tentativelyMergePatches should be the same as the final context of the
Sealed (FL Prim C(u)).  But,

Supposing we have a SealedRIO, that hides the resulting tentative
recorded state:

tentativelyMergePatches :: ... -> SealedRIO p C(r u t) (Sealed (FL Prim C(u)))

Wouldn't this create problems for the caller?  I think the two sealed
types are meant to be equal.

Or perhaps we should give the type a name and add an unsafeCoerce# in
the right places to quiet the complains about escaping existential
types.  I think it's the only place this comes up at the moment.

Jason


More information about the darcs-users mailing list