Designing programming languages that enable intuitive and safe manipulation of data structures is a critical research challenge. Conventional destructive memory operations using pointers are complex and prone to errors. Existing type systems, such as affine types and shape types, address this problem towards safe manipulation of heaps and pointers, but design of high-level declarative languages that allow us to manipulate complex pointer data structures at a higher level of abstraction is largely an open problem. The $λ_{GT}$ language, a purely functional programming language that treats hypergraphs (hereafter referred to as graphs) as primary data structures, addresses some of these challenges. By abstracting data with shared references and cycles as graphs, it enables declarative operations through pattern matching and leverages its type system to guarantee safety of these operations. Nevertheless, the previously proposed type system of $λ_{GT}$ leaves two significant open challenges. First, the type system does not support \emph{incomplete graphs}, that is, graphs in which some elements are missing from the graphs of user-defined types. Second, the type system relies on dynamic type checking during pattern matching. This study addresses these two challenges by incorporating linear implication into the $λ_{GT}$ type system, while introducing new constraints to ensure its soundness.

翻译：设计能够直观且安全地操作数据结构的编程语言是一项关键的研究挑战。传统的基于指针的破坏性内存操作既复杂又容易出错。现有的类型系统（如仿射类型和形状类型）针对堆和指针的安全操作提出了解决方案，但如何设计高级声明式语言，使我们能够在更高抽象层次上操作复杂的指针数据结构，在很大程度上仍是一个未解决的问题。λ_{GT}语言作为一种纯函数式编程语言，将超图（以下简称图）作为主要数据结构，部分解决了这些挑战。该语言通过将具有共享引用和循环的数据抽象为图，实现了基于模式匹配的声明式操作，并利用其类型系统保证这些操作的安全性。然而，先前提出的λ_{GT}类型系统仍存在两个重要的开放性问题：首先，该类型系统不支持不完全图，即用户定义类型的图中某些元素缺失的情况；其次，其类型系统在模式匹配过程中依赖动态类型检查。本研究通过在线性λ_{GT}类型系统中引入线性蕴含类型，并附加新的约束条件以确保其可靠性，从而解决了这两个问题。