Type Correct Changes: A Safe Approach to Version Control Implementation

  • Date  Time
  • Speaker
  • Location

Tuesday’s tech talk was a special treat, with Jason Dagit dropping by to talk about using GADTs to clean up the darcs patch theory implementation. (.pdf slides).Patch TheoryLogistics

  • Tuesday, Oct 14, 2008, 10.30 – 11.30


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.darcsWe 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.

Galois has been holding weekly technical seminars for several years on topics from functional programming, formal methods, compiler and language design, to cryptography, and operating system construction, with talks by many figures from the programming language and formal methods communities.