We propose to extend the concept of difference lists to general data structures and call them difference data structures. Difference lists
are well-known in logic programming as a data structure that realizes constant-time concatenation by retaining a reference to the tail as
well as the head of the list. In recent years, they are also called list segments and appear as a typical example of separation logic, a
logic for handling heaps and pointers. Difference data structures can be utilized to discuss various important concepts in programming
languages including functions, evaluation contexts, and continuations, in a unified setting. To handle such structures succinctly and
safely, we base this work on a graph rewriting language. We propose a typing method for graph rewriting languages based on graph grammar,
which covers structures beyond algebraic data types, to allow users to define difference data types for two different major applications,
i.e., (i) users can describe powerful pattern matching with user-defined shapes and (ii) the implementation can statically type-check operations on difference data structures efficiently. Our method introduces the concept of difference at the meta-level, i.e., difference data types are automatically derived from the base data type defined by graph grammar so that we can treat the base structure and difference structure uniformly without type conversion.

The presentation will be based on the PPDP2204 talk with emphasis on motivations and backgrounds.