Structural subtyping and parametric polymorphism provide similar flexibility and reusability to programmers. For example, both features enable the programmer to provide a wider record as an argument to a function that expects a narrower one. However, the means by which they do so differs substantially, and the precise details of the relationship between them exists, at best, as folklore in literature. In this paper, we systematically study the relative expressive power of structural subtyping and parametric polymorphism. We focus our investigation on establishing the extent to which parametric polymorphism, in the form of row and presence polymorphism, can encode structural subtyping for variant and record types. We base our study on various Church-style $\lambda$-calculi extended with records and variants, different forms of structural subtyping, and row and presence polymorphism. We characterise expressiveness by exhibiting compositional translations between calculi. For each translation we prove a type preservation and operational correspondence result. We also prove a number of non-existence results. By imposing restrictions on both source and target types, we reveal further subtleties in the expressiveness landscape, the restrictions enabling otherwise impossible translations to be defined. More specifically, we prove that full subtyping cannot be encoded via polymorphism, but we show that several restricted forms of subtyping can be encoded via particular forms of polymorphism.


翻译:结构子类型化和参数多态为程序员提供了相似的灵活性和可重用性。例如,两种特性都允许程序员将更宽的记录作为参数传递给期望更窄记录的函数。然而,它们实现这一目标的方式存在显著差异,且二者之间关系的精确细节充其量仅作为学术界的传说存在。本文系统研究了结构子类型化与参数多态的相对表达能力。我们聚焦于探究以行多态和存在多态形式呈现的参数多态能在多大程度上编码变体类型和记录类型的结构子类型化。研究基于多种扩展了记录与变体的Church风格λ演算、不同形式的结构子类型化以及行多态与存在多态。通过展示演算之间的组合翻译来刻画表达能力,并为每种翻译证明类型保持性和操作对应性结果。我们还证明了若干不存在性结果。通过对源类型和目标类型施加限制,揭示了表达能力图景中更微妙的细节——这些限制使得原本不可能的翻译得以定义。具体而言,我们证明了完全子类型化无法通过多态编码,但展示了若干受限形式的子类型化可通过特定形式的多态进行编码。

0
下载
关闭预览

相关内容

FlowQA: Grasping Flow in History for Conversational Machine Comprehension
专知会员服务
34+阅读 · 2019年10月18日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
60+阅读 · 2019年10月17日
《DeepGCNs: Making GCNs Go as Deep as CNNs》
专知会员服务
32+阅读 · 2019年10月17日
Keras François Chollet 《Deep Learning with Python 》, 386页pdf
专知会员服务
164+阅读 · 2019年10月12日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
41+阅读 · 2019年10月9日
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
STRCF for Visual Object Tracking
统计学习与视觉计算组
15+阅读 · 2018年5月29日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
From Softmax to Sparsemax-ICML16(1)
KingsGarden
74+阅读 · 2016年11月26日
国家自然科学基金
2+阅读 · 2017年12月31日
国家自然科学基金
13+阅读 · 2017年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
47+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
Arxiv
0+阅读 · 2023年10月25日
Arxiv
0+阅读 · 2023年10月25日
Arxiv
0+阅读 · 2023年10月24日
Arxiv
0+阅读 · 2023年10月23日
Arxiv
23+阅读 · 2022年2月24日
Arxiv
31+阅读 · 2021年6月30日
Arxiv
38+阅读 · 2020年12月2日
Learning Implicit Fields for Generative Shape Modeling
Arxiv
11+阅读 · 2018年12月6日
VIP会员
最新内容
马赛克战:俄乌战场透析
专知会员服务
11+阅读 · 今天4:12
《利用人工智能增强军事决策》
专知会员服务
2+阅读 · 今天4:09
《自动机器学习在军事数据耕耘法中的应用》
专知会员服务
4+阅读 · 今天4:02
为何指挥所生存能力要求范式转变
专知会员服务
2+阅读 · 今天3:54
打造“新蛛网”模式与高科技动员
专知会员服务
2+阅读 · 今天3:33
“蛛网”行动一周年:远程无人机战争
专知会员服务
2+阅读 · 今天3:23
【剑桥博士论文】智能体-环境协同优化
专知会员服务
6+阅读 · 6月9日
为初级军官战术训练设计生成式人工智能平台
专知会员服务
8+阅读 · 6月9日
《美军条令:作战伤员后送保障》
专知会员服务
6+阅读 · 6月9日
相关资讯
Hierarchically Structured Meta-learning
CreateAMind
27+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
29+阅读 · 2019年5月18日
强化学习的Unsupervised Meta-Learning
CreateAMind
18+阅读 · 2019年1月7日
Unsupervised Learning via Meta-Learning
CreateAMind
44+阅读 · 2019年1月3日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
18+阅读 · 2018年12月24日
STRCF for Visual Object Tracking
统计学习与视觉计算组
15+阅读 · 2018年5月29日
Hierarchical Imitation - Reinforcement Learning
CreateAMind
19+阅读 · 2018年5月25日
Focal Loss for Dense Object Detection
统计学习与视觉计算组
12+阅读 · 2018年3月15日
IJCAI | Cascade Dynamics Modeling with Attention-based RNN
KingsGarden
13+阅读 · 2017年7月16日
From Softmax to Sparsemax-ICML16(1)
KingsGarden
74+阅读 · 2016年11月26日
相关论文
Arxiv
0+阅读 · 2023年10月25日
Arxiv
0+阅读 · 2023年10月25日
Arxiv
0+阅读 · 2023年10月24日
Arxiv
0+阅读 · 2023年10月23日
Arxiv
23+阅读 · 2022年2月24日
Arxiv
31+阅读 · 2021年6月30日
Arxiv
38+阅读 · 2020年12月2日
Learning Implicit Fields for Generative Shape Modeling
Arxiv
11+阅读 · 2018年12月6日
相关基金
国家自然科学基金
2+阅读 · 2017年12月31日
国家自然科学基金
13+阅读 · 2017年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
47+阅读 · 2015年12月31日
国家自然科学基金
2+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
2+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员