发表机构
University of Strathclyde（思克莱德大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文针对高级函数式语言中数据类型运行时表示控制不足的问题，提出以交换 rig 为模型来描述数据类型的布局与变换，实现了数据同构及嵌入的建模。
AI 中文摘要
在高级函数式语言中，编译器通常几乎不给用户控制数据类型的运行时表示的权限。然而，出于效率或遗留原因，我们在程序层对数据结构的建模方式可能与我们希望在二进制层对其的表示方式不同。因此，能够描述数据类型的数据布局及其变换是编程中有用且必要的部分，但要做到正确、高效且易用却很困难。我们提出了有限代数数据类型的模型，将其视为交换 rig（无加法逆元的环），其中 rig 等式由数据之间的同构建模。使用此方法，我们还可以将数据类型嵌入更大的类型（例如位填充）建模为部分同构。
英文摘要
In high-level functional languages, the compiler often gives users little control over the runtime representation of data types. Yet how we model data structures at the program level can be different to how we want to represent them at the binary level, for efficiency or legacy reasons. Hence being able to describe data layouts and their transformations for data types is a useful and necessary part of programming, but difficult to do correctly, efficiently and ergonomically. We present a model of finite algebraic data types as a commutative rig (a ring without additive inverses), where the rig-equalities are modelled by isomorphisms between data. Using this approach, we can also model embedding a data type into a larger type (e.g. bit-padding) as a partial isomorphism.
