paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Intensional Functions

内涵函数
OOPSLA 8(OOPSLA2)2024匹配度 1/10 · 该论文属于纯程序语言设计与类型理论,讨论内涵函数、去函数化与内涵 monad,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析,与用户当前核心研究问题几乎没有交集。引用 0 inbox
Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu
dblp: 2026-09-10crossref: 2026-09-10

AI 速览

一句话:提出内涵函数语言特性,使函数可按定义位置与闭包捕获值定义非应用操作,并扩展出内涵 monad。

函数式语言中的函数只有应用这一消除形式,无法被比较、哈希或去重;现有 defunctionalization 需把函数转为一阶数据并手工改写调用,繁琐且使代码晦涩。本文提出内涵函数语言特性,允许依据函数的定义位置与闭包捕获值定义非应用操作,从而无需繁琐变换即可对这些函数实施一阶数据操作。作者给出操作语义与类型系统,证明其形式性质,并定义内涵 monad,使其 Kleisli 箭头为内涵函数,令 monadic 值也能接受额外操作。

问题
函数式语言中的函数仅能应用,无法直接比较、哈希或去重;defunctionalization 只能近似这些操作,且带来手工变换与维护负担。
方法
提出内涵函数,以定义位置和闭包捕获值定义非应用操作;给出操作语义与类型系统并证明形式性质,定义内涵 monad。
评估
以操作语义、类型系统和形式性质证明作为评估;摘要未给出实证基准或用户研究。
原文摘要(Abstract)

Functions in functional languages have a single elimination form — application — and cannot be compared, hashed, or subjected to other non-application operations. These operations can be approximated via defunctionalization: functions are replaced with first-order data and calls are replaced with invocations of a dispatch function. Operations such as comparison may then be implemented for these first-order data to approximate e.g. deduplication of continuations in algorithms such as unbounded searches. Unfortunately, this encoding is tedious, imposes a maintenance burden, and obfuscates the affected code. We introduce an alternative in intensional functions , a language feature which supports the definition of non-application operations in terms of a function’s definition site and closure-captured values. First-order data operations may be defined on intensional functions without burdensome code transformation. We give an operational semantics and type system and prove their formal properties. We further define intensional monads , whose Kleisli arrows are intensional functions, enabling monadic values to be similarly subjected to additional operations.

链接与引用

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

BibTeX
@article{PalmerFW24,
  title = {Intensional Functions},
  author = {Zachary Palmer and Nathaniel Wesley Filardo and Ke Wu},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {8},
  number = {OOPSLA2},
  year = {2024},
  doi = {10.1145/3689714}
}