Academic
Publications
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,Conor McBride

The Derivative of a Regular Type is its Type of One-Hole Contexts   (Citations: 17)
BibTex | RIS | RefWorks Download
Polymorphic regular types are tree-like datatypes gen- erated 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 with free, this paper shows a way to represent the one-hole contexts for elements of within elements of , together with an operation which will plug an element of into the hole of such a context. One-hole contexts are given as inhabitants of a regular type , computed generically from the syntactic struc- ture of by a mechanism better known as partial differ- entiation. 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-elementsof recursive types in a manner similar to Huet's 'zippers'(Hue97).
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
    • ...Although the present paper concerns only binary trees, we believe that the present work can be generalized to more varieties of data structures, based on the general zipper-like data structures as investigated in [1, 11]...

    Yuta Ikedaet al. Calculating tree navigation with symmetric relational zipper

    • ...The generic construction, observed in [32] has been implemented in Generic Haskell [24], and in Epigram [35]...

    Peter Morriset al. Indexed Containers

    • ...Epigram is described in more detail elsewhere, see [32] for a definition of the language with many applications, [11] for a short and more recent overview and [31] for an introductory tutorial...
    • ...As observed by McBride [29], the zipper is closely related to the notion of the derivative of a datatype, which has many structural similarities to derivatives in calculus...

    Thorsten Altenkirchet al. Generic Programming with Dependent Types

    • ...Finally, we equip the regular universe with the partial derivative which can be interpreted functionally as Huet’s notion of ‘zipper’, as suggested by McBride in [27] and implemented (without the fixpoint case) in Generic Haskell by Hinze, Jeuring and L¨oh [18]...
    • ...In the last example McBride’s observation [27], given its explanation in [3], has finally become a program...
    • ...As McBride observed [27], dierentiating a regular tree type T with respect to a free variable X computes the type of one-hole contexts for a value from X in a value from T. The explanation of the derivative as coding for the linear part of a polymorphic function space between containers can be found in [3]...

    Peter Morriset al. Exploring the Regular Tree Types

    • ...In a recent paper [15], Conor McBride linked the transformation from functor F to functor G to formal partial dierentiation...

    Gerard Huet. Linear Contexts and the Sharing Functor: Techniques for Symbolic Compu...

Sort by: