Galois Tech Talk: Type Correct Changes: A Safe Approach to Version Control Implementation October 14, 2008

Next week’s tech talk, a special treat, with Jason Dagit dropping by to talk about using GADTs to clean up the darcs patch theory implementation.

Logistics

* Tuesday, Oct 14, 2008, 10.30 - 11.30

Abstract

Darcs is based on a data model, known as Patch Theory, that sets it apart from other version control systems. The power of this data model is that it allows Darcs to manage significant complexity with a relatively straightforward user interface.

We show that Generalized Algebraic Data Types (GADTs) can be used to express several fundamental invariants and properties derived from Patch Theory. This gives our compiler, GHC, a way to statically enforce our adherence to the essential rules of our data model.

Finally, we examine how these techniques can improve the quality of the darcs codebase in practice.

Official Website: http://www.galois.com/blog/2008/10/09/type-correct-changes-a-safe-approach-to-version-control-implementation/