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