论文标题
通过切片类别的一阶仿射归纳数据类型的语义
Semantics for first-order affine inductive data types via slice categories
论文作者
论文摘要
仿射类型系统是限制信息复制的子结构类型系统，但在所有类型中都允许丢弃信息。这种类型的系统非常适合描述量子编程语言，因为复制量子信息违反了量子力学定律。在本文中，我们考虑了具有诱导数据类型的一阶仿射类型系统，并为其提供了一种新颖的分类语义。这种解释的最具挑战性的方面源于要求为我们的数据类型构建适当的丢弃地图，这些图可能由相互/嵌套的递归定义。我们通过采用一阶线性类型系统的模型，其原子类型是可以丢弃的，然后使用张量单元在模型类别中对类型的类型进行额外的仿射解释来展示如何实现这一目标。我们为从古典到量子的语言提供了一些具体的分类模型。最后，我们讨论了划定和扩展我们的方法的潜在方法，并将其用于解释煤层和懒惰的数据类型。
Affine type systems are substructural type systems where copying of information is restricted, but discarding of information is permissible at all types. Such type systems are well-suited for describing quantum programming languages, because copying of quantum information violates the laws of quantum mechanics. In this paper, we consider a first-order affine type system with inductive data types and present a novel categorical semantics for it. The most challenging aspect of this interpretation comes from the requirement to construct appropriate discarding maps for our data types which might be defined by mutual/nested recursion. We show how to achieve this for all types by taking models of a first-order linear type system whose atomic types are discardable and then presenting an additional affine interpretation of types within the slice category of the model with the tensor unit. We present some concrete categorical models for the language ranging from classical to quantum. Finally, we discuss potential ways of dualising and extending our methods and using them for interpreting coalgebraic and lazy data types.
