一句话:提出 Flix 中语言集成 Datalog 的设计,使 Datalog 程序可模块化、多态、类型化地复用于程序分析等任务。
论文综述 Flix 编程语言中的 Datalog 设施。问题在于如何在通用语言中以模块化、可复用且类型安全的方式编写和组合 Datalog 程序。方法上,Flix 将 Datalog 程序作为一等值,引入 rho 抽象、参数多态和类型类,并提供 inject/query 程序构造、head/guard 表达式、函数式谓词和格语义等特性,从而增强表达力与易用性。评估上,作者用 Ullman 分层算法、Ford-Fulkerson 最大流以及上下文敏感程序分析中的 IFDS 和 IDE 算法等应用进行说明,并给出这些算法的完全模块化、多态、类型化与声明式实现,可实例化到任意抽象域。
We present a comprehensive overview of the Datalog facilities in the Flix programming language. We show how programmers can write functions implemented as Datalog programs and we demonstrate how to build modular and reusable families of Datalog programs using first-class Datalog program values, rho abstraction, parametric polymorphism, and type classes. We describe several features that improve the ergonomics, flexibility, and expressive power of Datalog programming in Flix, including the inject and query program constructs, head and guard expressions, functional predicates, lattice semantics, and more. We illustrate Datalog programming in Flix with several applications, including implementations of Ullman's algorithm to stratify Datalog programs, the Ford-Fulkerson algorithm for maximum flow, and the IFDS and IDE algorithms for context-sensitive program analysis. The implementations of IFDS and IDE fulfill a long-term goal: to have fully modular, polymorphic, typed, and declarative formulations of these algorithms that can be instantiated with any abstract domain.