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代码。