Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(3)
Fixed Point
Polymorphism
Recursive Types
Subscribe
Academic
Publications
The Derivative of a Regular Type is its Type of OneHole Contexts
The Derivative of a Regular Type is its Type of OneHole Contexts,Conor McBride
Edit
The Derivative of a Regular Type is its Type of OneHole Contexts
(
Citations: 17
)
BibTex

RIS

RefWorks
Download
Conor McBride
Polymorphic regular types are treelike 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 onehole contexts for elements of within elements of , together with an operation which will plug an element of into the hole of such a context. Onehole 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 onehole contexts for subelementsof
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.
(
strictlypositive.org
)
(
reference.kfupm.edu.sa
)
(
www.cs.nott.ac.uk
)
Citation Context
(7)
...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 zipperlike data structures as investigated in [1,
11
]...
Yuta Ikeda
,
et 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 Morris
,
et 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 Altenkirch
,
et 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 onehole 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 Morris
,
et 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...
References
(5)
Inductive sets and families in Martin  L¨of''''s type theory
(
Citations: 26
)
P. Dybjer
Published in 1991.
PolyPa polytypic programming language extension
(
Citations: 157
)
Patrik Jansson
,
Johan Jeuring
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, 1997
Dependently Typed Functional Programs and their Proofs
(
Citations: 82
)
Conor McBride
Published in 1999.
The Zipper
(
Citations: 77
)
Gérard P. Huet
Journal:
Journal of Functional Programming  JFP
, vol. 7, no. 5, pp. 549554, 1997
Foncteurs analytiques et espec`es de structures
(
Citations: 57
)
A. Joyal
Published in 1986.
Sort by:
Citations
(17)
Calculating tree navigation with symmetric relational zipper
Yuta Ikeda
,
Susumu Nishimura
Conference:
Partial Evaluation and SemanticBased Program Manipulation  PEPM
, pp. 101110, 2011
Species and functors and types, oh my!
Brent A. Yorgey
Published in 2010.
Indexed Containers
(
Citations: 10
)
Peter Morris
,
Thorsten Altenkirch
Conference:
Logic in Computer Science  LICS
, pp. 277285, 2009
The third homomorphism theorem on trees: downward & upward lead to divideandconquer
(
Citations: 5
)
Akimasa Morihata
,
Kiminori Matsuzaki
,
Zhenjiang Hu
,
Masato Takeichi
Conference:
ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL
, pp. 177185, 2009
The third homomorphism theorem on trees: downward & upward lead to divideandconquer
Akimasa Morihata
,
Kiminori Matsuzaki
,
Zhenjiang Hu
,
Masato Takeichi
Journal:
Sigplan Notices  SIGPLAN
, vol. 44, no. 1, pp. 177185, 2009