一句话：利用 container morphism 将多态程序转换为可自动推理的形式，从而基于输入输出示例判定多态规约的可实现性。
多态函数受参数性约束：Wadler 自由定理可作为免费规约，把部分规约补全为全规约，也可能使原本可实现的规约变为不可实现；在程序合成中，判定不可实现性可剪枝搜索空间。本文研究参数性、输入输出示例与 sketch 的交互。由于自由定理引入全称量化函数，自动推理困难，作者采用 container morphism 作为多态函数的替代表示，以更可操作的方式刻画参数性，并把程序翻译到 container 设定。结果表明，带输入输出示例的多态程序可实现性推理可以被自动化。
Parametricity states that polymorphic functions behave the same regardless of how they are instantiated. When developing polymorphic programs, Wadler’s free theorems can serve as free specifications, which can turn otherwise partial specifications into total ones, and can make otherwise realizable specifications unrealizable. This is of particular interest to the field of program synthesis, where the unrealizability of a specification can be used to prune the search space. In this paper, we focus on the interaction between parametricity, input-output examples, and sketches. Unfortunately, free theorems introduce universally quantified functions that make automated reasoning difficult. Container morphisms provide an alternative representation for polymorphic functions that captures parametricity in a more manageable way. By using a translation to the container setting, we show how reasoning about the realizability of polymorphic programs with input-output examples can be automated.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2406-18304,
title = {Example-Based Reasoning about the Realizability of Polymorphic Programs},
author = {Niek Mulleners and Johan Jeuring and Bastiaan Heeren},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {ICFP},
year = {2024},
doi = {10.1145/3674636}
}