论文标题
（深）GADT的功能如何？
How Functorial Are (Deep) GADTs?
论文作者
论文摘要
众所周知，GADT不接受ADT和嵌套类型支持的标准图功能。此外，标准地图函数不足以在深度GADT的元素中，甚至只是深度ADT或嵌套类型的元素中的所有结构上分配其数据改变的参数函数。本文开发了一种用于准确检测哪些功能的算法，该函数与（深）GADT的数据相对于数据。该算法将输入术语t作为输入t，其类型是深度GADT d的实例，并且要在t上映射的函数f。它检测到最小的t形状作为D的元素，并且返回一组最小的约束F必须满足以在t上映射。该算法的症结在于它的能力将T的基本结构分为D的元素，即T的部分对于它具有D的形状与d-元素的形状至关重要的部分，即其作为d的元素元素，即t的元素，即仅在这种形状的位置中的数据。该算法可确保F上的约束仅来自T的基本结构。这项工作是为GADT定义初始代数语义的持续努力的一部分，该语义适当地将ADT和嵌套类型的常规语义概括为高阶内functors的最小固定点。
It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all of the structure present in elements of deep GADTs, even just deep ADTs or nested types. This paper develops an algorithm for detecting exactly which functions are mappable over data whose types are (deep) GADTs. The algorithm takes as input a term t whose type is an instance of a deep GADT D and a function f to be mapped over t. It detects a minimal possible shape of t as an element of D, and returns a minimal set of constraints f must satisfy to be mappable over t. The crux of the algorithm is its ability to separate t's essential structure as an element of D -- i.e., the part of t that is essential for it to have the shape of an element of D -- from its incidental structure as an element of D -- i.e., the part of t that is simply data in the positions of this shape. The algorithm ensures that the constraints on f come only from t's essential structure. This work is part of an ongoing effort to define initial algebra semantics for GADTs that properly generalizes the usual semantics for ADTs and nested types as least fixpoints of higher-order endofunctors.
