The derivative of a regular type is its type of one-hole contexts Export

@misc{citeulike:2492206, abstract = {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 `equality 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 ...}, author = {Mcbride, C.}, citeulike-article-id = {2492206}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.8611}, keywords = {derivative, type}, posted-at = {2008-03-09 03:10:43}, priority = {2}, title = {The derivative of a regular type is its type of one-hole contexts}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.8611}, year = {2001} }

TY - GEN ID - citeulike:2492206 L3 - citeulike-article-id:2492206 N2 - 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 `equality 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 ... TI - The derivative of a regular type is its type of one-hole contexts KW - derivative KW - type AU - Mcbride, C PY - 2001/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.22.8611 ER -