Structural subtyping and parametric polymorphism provide a similar kind of flexibility and reusability to programmers. For example, both enable the programmer to supply 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.


翻译:结构子类型和参数化多态都为程序员提供了类似的灵活性和可重用性。例如,两者都使程序员能够将更宽的记录作为参数传递给期望更窄的记录的函数。然而,它们实现的方式存在很大差异,并且它们之间的关系的确切细节在文献中至多是民间故事。在本文中,我们系统地研究了结构子类型和参数化多态的相对表达能力。我们的关注点在于建立参数化多态(以行和存在多态的形式)可以为变量和记录类型编码结构子类型的程度。我们基于包含记录和变量的不同形式的结构子类型和行和存在多态的各种 Church 风格 $\lambda$-演算研究了这个问题。我们通过展示演算之间的组合翻译来表征表达能力。针对每个翻译,我们证明了类型保持和操作对应结果。我们还证明了一些不存在的结果。通过对源类型和目标类型施加限制,我们揭示了表达能力领域中的进一步细微差别,这些限制使得原本不可能的翻译得以定义。

0
下载
关闭预览

相关内容

MIT最新《贝叶斯深度学习》综述论文,37页pdf
专知会员服务
50+阅读 · 2021年1月4日
【图神经网络(GNN)结构化数据分析】
专知会员服务
115+阅读 · 2020年3月22日
【论文】结构GANs,Structured GANs,
专知会员服务
14+阅读 · 2020年1月16日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
代码重构:面向单元测试
阿里技术
0+阅读 · 2022年7月29日
【ACL2020放榜!】事件抽取、关系抽取、NER、Few-Shot 相关论文整理
深度学习自然语言处理
18+阅读 · 2020年5月22日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
全球人工智能
19+阅读 · 2017年12月17日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Arxiv
0+阅读 · 2023年6月1日
Arxiv
13+阅读 · 2019年11月14日
Arxiv
19+阅读 · 2018年10月25日
VIP会员
相关资讯
代码重构:面向单元测试
阿里技术
0+阅读 · 2022年7月29日
【ACL2020放榜!】事件抽取、关系抽取、NER、Few-Shot 相关论文整理
深度学习自然语言处理
18+阅读 · 2020年5月22日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
vae 相关论文 表示学习 1
CreateAMind
12+阅读 · 2018年9月6日
ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
全球人工智能
19+阅读 · 2017年12月17日
【推荐】ResNet, AlexNet, VGG, Inception:各种卷积网络架构的理解
机器学习研究会
20+阅读 · 2017年12月17日
Capsule Networks解析
机器学习研究会
11+阅读 · 2017年11月12日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
【论文】图上的表示学习综述
机器学习研究会
14+阅读 · 2017年9月24日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2013年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2012年12月31日
国家自然科学基金
0+阅读 · 2008年12月31日
Top
微信扫码咨询专知VIP会员