Introducing Linear Implication Types to λGT for Computing With Incomplete Graphs

Designing programming languages that support intuitive and safe manipulation of complex data structures remains a fundamental research challenge. The λGT language addresses this challenge by treating hypergraphs (hereafter simply referred to as graphs) as first-class data structures in a purely functional setting. By representing data as graphs, λGT naturally captures sharing and cyclic structures. Moreover, the language provides declarative graph manipulation through pattern matching, and its type system is designed to guarantee the safety of such operations. Nevertheless, the previously proposed type system of λGT still suffers from two fundamental limitations. The first limitation is the lack of support for incomplete graphs, that is, graphs in which some components are missing from the graphs of user-defined types. Such incomplete graphs arise naturally in practice, in particular as intermediate graphs during pattern matching. The second limitation is the reliance on dynamic type checking during pattern matching. Naively eliminating dynamic checks leads to unsoundness, leaving fully static type checking as an open problem. This paper addresses both limitations. To overcome the first limitation, we extend the type system of λGT with linear implication types, which enable the typing of incomplete graphs. To address the second limitation, we introduce additional constraints on both case patterns and types to eliminate the need for dynamic type checking while preserving soundness.