Grassroots Logic Programs (GLP) is a concurrent logic programming language in which logic variables are partitioned into paired readers and writers. An assignment is produced at most once via a writer and consumed at most once via its paired reader, and may contain additional readers and/or writers. This enables the concise expression of rich multidirectional communication modalities. ``Logic Programs as Types for Logic Programs'' (LICS'91) defined types as regular sets of paths over derivable ground atoms. Here, we define types to be regular sets of moded paths, where a mode captures directionality of communication -- whether a subterm is consumed from or produced to the environment -- enabling the typing of interactive partial computations including those that eventually deadlock or fail, or never terminate. We provide a syntactic definition of well-typing and prove that a program is well-typed iff the path abstraction of its moded-atom semantics satisfies covariance and contravariance conditions with respect to its type. The GLP type system was implemented in Dart by AI, starting from a mathematical specification of Typed GLP (this paper), deriving from it an English spec (written by AI), and from the spec deriving Dart code (by AI). While GLP is naturally untyped, the motivation for Typed GLP comes from programming with AI: Asking AI to program complex communication modalities in GLP (and in general) and hoping for the best is a tenuous strategy. The emerging discipline we advocate and employ is for the human designer and AI to jointly develop and agree upon (1)~GLP types; (2)~GLP procedure type declarations; (3)~informal (English) descriptions of the procedures; and only then let AI attempt to write (4)~GLP code based on those.

翻译：基层逻辑程序（GLP）是一种并发逻辑编程语言，其中逻辑变量被划分为配对的读取器和写入器。赋值通过写入器至多产生一次，并通过其配对的读取器至多消费一次，且可能包含额外的读取器和/或写入器。这使得丰富的多向通信模式能够被简洁地表达。《逻辑程序作为逻辑程序的类型》（LICS'91）将类型定义为可推导基原子上的正则路径集合。在此，我们将类型定义为模态路径的正则集合，其中模态捕捉通信的方向性——即子项是从环境消费还是向环境产生——从而能够对交互式部分计算进行类型化，包括那些最终死锁、失败或永不终止的计算。我们给出了良类型化的语法定义，并证明一个程序是良类型化的当且仅当其模态原子语义的路径抽象相对于其类型满足协变和逆变条件。GLP类型系统由AI在Dart中实现，从《类型化GLP》（本文）的数学规范出发，推导出英文规范（由AI撰写），并从该规范推导出Dart代码（由AI生成）。虽然GLP本质上是无类型的，但类型化GLP的动机源于与AI协同编程：要求AI在GLP（及一般意义上）中编写复杂的通信模式并寄望于最佳结果是一种脆弱的策略。我们倡导并采用的新兴方法是让人工设计者与AI共同开发并商定：（1）GLP类型；（2）GLP过程类型声明；（3）过程的非正式（英文）描述；然后才让AI尝试基于这些编写（4）GLP代码。