paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Flexible and Expressive Typed Path Patterns for GQL

面向 GQL 的灵活且富有表达力的带类型路径模式
OOPSLA 9(OOPSLA2)2025匹配度 3/10 · 该论文属于程序语言与静态分析/类型系统方向,提出了 GQL 查询的带不精确类型系统并形式化验证空查询与卡住查询,与用户在 PL 中关注静态分析和形式化方法有弱关联。但它不涉及机器学习系统、Agentic 程序、LLM 辅助静态分析、浮点程序分析或贝叶斯程序分析,因此与用户当前核心研究方向匹配度较低。引用 1 inbox
Wenjia Ye, Matías Toro, Tomás Díaz, Bruno C. d. S. Oliveira, Manuel Rigger, Claudio Gutierrez, Domagoj Vrgoč
crossref: 2026-09-10

AI 速览

一句话:为 GQL 核心片段提出带不精确类型的类型系统 FPPC,静态检测空查询与卡住查询并保证类型安全。

图数据库广泛应用促使 ISO 推出图查询语言 GQL 标准,但初版规范缺乏用于查询验证的形式化类型系统,导致查询可能因类型不一致在运行时失败,或静默返回空结果。本文为 GQL 的一个核心片段提出形式化类型模型 FPPC,并扩展了基于属性的过滤以及模式与查询两端的不精确类型。该模型能够静态检测语义上不正确或会卡住的查询,从而改善用户反馈。作者证明了若干关键理论性质:空性(检测由类型不匹配导致的空查询)与类型安全(保证良类型查询不会在运行时失败),并进一步证明渐进保证,即移除类型标注要么不引入静态类型错误,要么仅增大结果集。通过在 GQL 中引入不精确性,FPPC 为模式演化与不完整类型信息提供了灵活方案,提升了 GQL 的健壮性、可用性与形式化基础。

问题
GQL 标准初版缺少用于查询验证的形式化类型系统,查询可能因类型不一致在运行时失败或无声产生空结果。
方法
为 GQL 核心片段(含属性过滤与不精确类型)设计形式化类型模型 FPPC,并证明空性、类型安全与渐进保证等性质。
评估
以理论证明方式建立空性、类型安全与渐进保证等关键性质,论证该类型系统对查询静态检测与模式演化的支持。
原文摘要(Abstract)

Graph databases have become an important data management technology across various domains, including biology, sociology, industry ( e.g . fraud detection, supply chain management, financial services), and investigative journalism, due to their ability to efficiently store and query large-scale knowledge graphs and networks. Recently, the Graph Query Language (GQL) was introduced as a new ISO standard providing a unified framework for querying graphs. However, this initial specification lacks a formal type system for query validation. As a result, queries can fail at runtime due to type inconsistencies or produce empty results without prior warning. Solving this issue would help users write correct queries, especially on large datasets. To address this gap, we introduce a formal type model for a core fragment of GQL extended with property-based filtering and imprecise types both in the schema and the queries. This model, named FPPC, enables static detection of semantically incorrect and stuck queries, improving user feedback. We establish key theoretical properties, including emptiness (detecting empty queries due to type mismatches) and type safety (guaranteeing that well-typed queries do not fail at runtime). Additionally, we prove a gradual guarantee , ensuring that removing type annotations either does not introduce static type errors or only increases the result set. By integrating imprecision into GQL, FPPC offers a flexible solution for handling schema evolution and incomplete type information. This work contributes to making GQL more robust, improving both its usability and its formal foundation.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot2891,
  title = {Flexible and Expressive Typed Path Patterns for GQL},
  author = {Wenjia Ye and Matías Toro and Tomás Díaz and Bruno C. d. S. Oliveira and Manuel Rigger and Claudio Gutierrez and Domagoj Vrgoč},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {OOPSLA2},
  year = {2025},
  doi = {10.1145/3763061}
}