paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Handling the Selection Monad

处理选择单子(Selection Monad)
PLDI 9(PLDI)2025匹配度 1/10 · 该论文属于纯 PL 语言设计与形式语义方向,研究 selection monad、代数效应处理器及 λC 的操作/指称语义,未涉及 LLM/Agent、静态分析、浮点程序分析或贝叶斯程序分析,因此与用户当前研究画像基本无关。引用 1 inbox
Gordon Plotkin, Ningning Xie
crossref: 2026-09-10

AI 速览

一句话:提出带选择续延的代数效应处理器,使程序员能实现感知损失的选择操作,并给出λC语言的操作/指称语义与Haskell实现。

本文研究如何让程序员自定义选择操作,而非仅由选择单子给出最优选择。Abadi 与 Plotkin 曾用选择单子建模带损失感知的选择语言,但其选择是最优的,并留下程序员提供选择的问题。作者提出一种新设计:在代数效应处理器中,除定界续延外还加入选择续延,使操作可访问未来可能损失,从而实现感知损失的优化算法。文章为高阶模型语言 λC 给出操作语义,证明进展、类型可靠性和在带温和层级约束的操作类型子集上的终止性;并为该子集给出选择单子指称语义,证明可靠性与充分性。还提供 Haskell 实现和多个编程实例。

问题
Abadi 与 Plotkin 用选择单子建模的语言只支持最优选择;如何让选择由程序员提供,并保持类型安全与语义良好性?
方法
扩展代数效应处理器,在定界续延之外加入选择续延以暴露未来可能损失;定义高阶语言 λC 的操作语义与选择单子指称语义,并给出 Haskell 实现。
评估
证明 λC 的进展、类型可靠性和受限子集终止性,证明指称语义的可靠性与充分性,并通过 Haskell 编程实例展示设计可用性。
原文摘要(Abstract)

The selection monad on a set consists of selection functions. These select an element from the set, based on a loss (dually, reward) function giving the loss resulting from a choice of an element. Abadi and Plotkin used the monad to model a language with operations making choices of computations taking account of the loss that would arise from each choice. However, their choices were optimal, and they asked if they could instead be programmer provided. In this work, we present a novel design enabling programmers to do so. We present a version of algebraic effect handlers enriched by computational ideas inspired by the selection monad. Specifically, as well as the usual delimited continuations, our new kind of handlers additionally have access to choice continuations , that give the possible future losses. In this way programmers can write operations implementing optimisation algorithms that are aware of the losses arising from their possible choices. We give an operational semantics for a higher-order model language λC , and establish desirable properties including progress, type soundness, and termination for a subset with a mild hierarchical constraint on allowable operation types. We give this subset a selection monad denotational semantics, and prove soundness and adequacy results. We also present a Haskell implementation and give a variety of programming examples.

链接与引用

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

BibTeX
@article{paperbot3142,
  title = {Handling the Selection Monad},
  author = {Gordon Plotkin and Ningning Xie},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {9},
  number = {PLDI},
  year = {2025},
  doi = {10.1145/3729321}
}