[Haskell-cafe] A suggestion: On why code merges should influence Haskell design

David Turner dct25-561bs at mythic-beasts.com
Mon Oct 12 20:16:13 UTC 2015


I work on a team of ~15 developers and we follow a merge-free process using
rebasing. Although in theory it sounds like you'll get the same problems
with rebasing as with merging, over 6 years and 100,000+ commits I'm
struggling to think of a single bug silently introduced due to a rebase
that succeeded without conflicts. It's a cunning bit of social engineering:
when merging the work of two developers, it's easy for both of them to
disclaim responsibility for any bugs introduced by the merge, but when
rebasing the work of developer A on top of that of developer B it's clear
that any bugs are dev A's responsibility as their commits come later in the
published history than dev B's, and this gives dev A the incentive to check
for semantic conflicts properly.

That said, it's theoretically possible to introduce bugs with a 'clean'
rebase, just as with merging, and I'm interested in your suggestion because
of that. The difficulty I see is defining what you mean by "no new bugs".
The two branches satisfy two different specifications, and my reading of
"no new bugs" is that the merge result satisfies a merged specification. It
sounds difficult to automatically merge two specs together in general,
although in practice specs are often quite informal and where a rebase
looks questionable a merged spec can be invented and verified with human
intervention, remembering that the rebasing developer has a personal
incentive to get this right.

There's two kind of formal spec that I know of in common usage in the
industry: types and tests. Using a type system gives you a bunch of
theorems about what your program can and cannot do, and this is checked at
compile time, and an automated test suite is basically a bunch of
properties that your program satisfies which can be verified by running the
test suite. Neither of these can capture the real spec exactly, but in
practice they turn out to be good enough for many purposes. For those cases
where that's not enough you can bring out the heavy artillery of a theorem
prover, and this does let you write down the real spec exactly and verify
it either side of a merge or rebase. I wouldn't say that approach was in
common usage but it does get used where the investment is worth it.

Verifying that changes to the type system leave the real spec satisfied
sounds quite hard in general. Merging additions to the test suite sounds
easy but other changes to the part of the spec embodied in the test suite
also sounds hard in general. Of the three, merging changes to an
automatically-proved theorem actually feels easiest - my experience is that
keeping a (well-written) automatic proof in sync with changes to code is
often not that hard, and when it is hard it's normally been because the
changes to the code meant the theorem was no longer true.

Perhaps enriching the type system to a point where you can write truly
useful specs in it is the answer? Thus dependent types.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20151012/47b46056/attachment.html>

More information about the Haskell-Cafe mailing list