[darcs-devel] Context witnesses of the Repository type

[Ben Franksen]

Ganesh Sittampalam wrote:
> On 16/06/2015 01:03, Ben Franksen wrote:
>> I have done a lot of poking into the deep and dark internals lately. One
>> thing that came up is that I started to wonder whether the witnesses of
>> the Repository type are really worth the bother. It appears to me that in
>> most cases they merely add noise to the type signatures and to the code
>> (to get one or more arguments in shape using ugly things like
>> unsafeCoerce*).
>> 
>> I'd be interested how this is perceived by others. Have the Repository
>> witnesses ever helped you to avoid making a mistake, for instance during
>> some refactoring? If yes, do you think they are valuable enough to
>> justify their cost (in code complexity and readability)?
> 
> Personally I like having them. I think they're useful documentation as
> well as providing some compiler checking - for me they actually make the
> code *more* readable because they give more information about what it's
> doing. For example I can see at a glance from the type of a function
> that it updates just the tentative state.

Hm, that would be useful. Can you point me to such a function and explain 
how I can see that from the type?

> I'm not sure if I can point to specific mistakes they've helped me
> avoid, but generally having good static types makes me more confident
> when refactoring.

In principle I agree completely.

But in this case I almost always see the same boring

  forall p wR wU wT. (<constraints for p>) => Repository p wR wU wT ...

that doesn't tell me much. Or does it?

> I think their biggest weakness is that we don't have a way of enforcing
> linearity at present: if you write something to disk, changing the
> witnesses, then the compiler doesn't do anything to prevent you re-using
> the old repository value with the old witnesses. I'd love to find a way
> to fix that.
> 
> http://bugs.darcs.net/issue2432 is a good example of this coming up in
> practice.

Ok, fair.

Cheers
Ben
-- 
"Make it so they have to reboot after every typo." ― Scott Adams