一句话:提出弹性表定义函数,将用户写定的定长数组函数自动泛化为可处理任意长度输入,并证明得到主泛化。
表定义函数(SDF)为电子表格带来了模块化与抽象,但终端用户往往只写出针对固定大小数组的函数,导致复用性受限。本文提出一种原则性方法,把这类 SDF 泛化为可处理任意大小输入的“弹性 SDF”。作者证明:在自然且可检查的条件下,其算法返回输入 SDF 的主泛化(principal generalisation),并给出了弹性 SDF 的形式语义与若干高效实现策略。评估方面,作者开展了一项面向电子表格用户的用户研究,将使用弹性 SDF 编程的体验与依赖 map/reduce 等数组处理组合子的替代方案进行对比。结果显示,弹性 SDF 的认知负荷低于使用 map/reduce 组合子的 SDF,而后者是最接近的替代方案。
Abstract Sheet-defined functions (SDFs) bring modularity and abstraction to the world of spreadsheets. Alas, end users naturally write SDFs that work over fixed-size arrays, which limits their reusability. To help end user programmers write more reusable SDFs, we describe a principled approach to generalising such functions to become elastic SDFs that work over inputs of arbitrary size. We prove that under natural, checkable conditions, our algorithm returns the principal generalisation of an input SDF. We describe a formal semantics and several efficient implementation strategies for elastic SDFs. A user study with spreadsheet users compares the human experience of programming with elastic SDFs to the alternative of relying on array-processing combinators. Our user study finds that the cognitive load of elastic SDFs is lower than for SDFs with map/reduce array combinators, the closest alternative solution.
@article{McCutchenBGJS20,
title = {Elastic sheet-defined functions: Generalising spreadsheet functions to variable-size input arrays},
author = {MATT MCCUTCHEN and JUDITH BORGHOUTS and ANDREW D. GORDON and SIMON PEYTON JONES and ADVAIT SARKAR},
journal = {Journal of Functional Programming},
volume = {30},
year = {2020},
doi = {10.1017/s0956796820000234}
}