结构子类型作为参数化多态

摘要:结构子类型和参数多态为程序员提供了类似的灵活性和可重用性。例如,两者都使程序员能够将较宽的记录作为参数传递给期望较窄记录的函数。然而,它们所采用的方式存在很大的区别,它们之间的关系的具体细节充其量只存在于文献传说中。 在本文中,我们系统地研究结构子类型和参数多态的相对表达能力。我们重点研究了参数多态在行和存在多态的形式中能否为变体和记录类型编码结构子类型的程度。我们基于不同形式的结构子类型、行和存在多态以及带有记录和变体的各种 Church-style lambda-演算进行研究。 我们通过展示不同演算之间的组合性翻译来表征表达能力。对于每个翻译,我们证明了类型保持和操作对应的结果。我们还证明了一些不存在的结论。通过对源类型和目标类型施加限制,我们揭示了表达能力景观中的进一步细微差别,这些限制使得原本不可能的翻译得以定义。

作者:Wenhao Tang, Daniel Hillerstr"om, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu, Sam Lindley

论文ID:2304.08267

分类:Programming Languages

分类简称:cs.PL

提交时间:2023-04-18

PDF 下载: 英文版 中文版pdf翻译中