Type checking data structures more complex than trees

TL;DR

This paper introduces a purely functional language, $ abla_{GT}$, with a new type system, $F_{GT}$, enabling safe, immutable handling and pattern matching of complex graph data structures like doubly-linked lists and skip lists.

Contribution

It presents a novel functional language and type system for handling complex graph data structures without destructive updates, simplifying verification.

Findings

Supports immutable graph data structures with pattern matching

Provides automatic property verification using a simple type system

Contrasts with traditional pointer analysis methods

Abstract

Graphs are a generalized concept that encompasses more complex data structures than trees, such as difference lists, doubly-linked lists, skip lists, and leaf-linked trees. Normally, these structures are handled with destructive assignments to heaps, which is opposed to a purely functional programming style and makes verification difficult. We propose a new purely functional language, $\lambda_{GT}$, that handles graphs as immutable, first-class data structures with a pattern matching mechanism based on Graph Transformation and developed a new type system, $F_{GT}$, for the language. Our approach is in contrast with the analysis of pointer manipulation programs using separation logic, shape analysis, etc. in that (i) we do not consider destructive operations but pattern matchings over graphs provided by the new higher-level language that abstract pointers and heaps away and that (ii) we pursue what properties can be established automatically using a rather simple typing framework.