Type-Directed Diffing of Structured Data

Victor Cacciari Miraldo, Pierre Evariste Dagand, Wouter Swierstra

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    Abstract

    The Unix diff utility that compares lines of text is used pervasively by version control systems. Yet certain changes to a program may be dicult to describe accurately in terms of modications to individual lines of code. As a result, observing changes at such a xed granularity may lead to unnecessary conicts between dierent edits. This paper presents a generic representation for describing transformations between algebraic data types and a non-deterministic algorithm for computing such representations. These representations can be used to give a more accurate account of modications made to algebraic data structures – and the abstract syntax trees of computer programs in particular – as opposed to only considering modications between their textual representations.
    Original languageEnglish
    Title of host publicationTyDe 2017
    Subtitle of host publicationProceedings of the 2nd ACM SIGPLAN International Workshop on Type-Driven Development
    PublisherAssociation for Computing Machinery
    Pages2–15
    Number of pages14
    ISBN (Print)978-1-4503-5183-6
    DOIs
    Publication statusPublished - 3 Sept 2017

    Keywords

    • Datatype Generic Programming
    • Version Control
    • Dependently typed programming
    • Agda

    Fingerprint

    Dive into the research topics of 'Type-Directed Diffing of Structured Data'. Together they form a unique fingerprint.

    Cite this