The Derivative of a Regular Type is its Type of One-Hole Contexts
The Derivative of a Regular Type is its Type of One-Hole Contexts
复制标题
正则类型的导数是其单孔上下文类型
DOI：
--
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Conor McBride
中科院分区：
文献类型：
--
作者：
Conor McBride
多态正则类型是由一组自由变量上的多项式类型表达式生成的树状数据类型，并在最小定点下封闭。Core ML 的 "等价类型 "可以用这种形式表示。给定这样一个带有 x 的自由类型表达式 T，本文展示了一种在 T 的元素中表示 x 元素的单孔上下文的方法，以及一种将 x 元素插入这种上下文的孔中的操作。单孔上下文是作为正则类型 @xT 的居民给出的，而正则类型 @xT 是由 T 的语法结构通过一种称为局部微分的机制计算出来的。相关的包含概念被证明可以用导数和插入来恰当地描述。然后利用这一技术，以类似于 Huet 的 "拉链"[Hue97] 的方式给出递归类型子元素的单孔上下文。
Polymorphic regular types are tree-like datatypes generated by polynomial type expressions over a set of free variables and closed under least fixed point. The ‘equal-ity types’ of Core ML can be expressed in this form. Given such a type expression T with x free, this paper shows a way to represent the one-hole contexts for elements of x within elements of T , together with an operation which will plug an element of x into the hole of such a context. One-hole contexts are given as inhabitants of a regular type @xT , computed generically from the syntactic structure of T by a mechanism better known as partial differentiation . The relevant notion of containment is shown to be appropriately characterized in terms of derivatives and plugging in. The technology is then exploited to give the one-hole contexts for sub-elements of recursive types in a manner similar to Huet’s ‘zippers’[Hue97].