Has anyone done an analysis to see if Blute, Cockett, and Seely's differential categories suffice to provide a notion of 1-hole context in the symmetric monoidal setting?
1
-
1$\begingroup$ At first sight, it seems like we are talking of two different notions of derivation here. In McBride's context, one considers the derivative of a type $A$ in order to get the type of one-hole contexts of type $A$. In the differential $\lambda$-calculus, one considers the derivative of a term $t$ of type $\mathop{!}A\multimap B$ obtaning a term of type $A\otimes\mathop{!}A\multimap B$ yielding the linear approximations of $t$ with respect to $x$. Although the two notions may perhaps be related at som level (they both linearize something), I am unsure whether there is a formal connection. $\endgroup$– Damiano MazzaCommented May 4, 2016 at 8:07
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
The beginnings of a connection have been made, but there is still quite a bit left to do. The key is to formulate data types as polynomial functors.
The history of polynomial functors is very well written up by Joachim Kock in
http://mat.uab.es/~kock/cat/polynomial.pdf
in which he mentions the many names that contributed to their development. Kock also describes how to model data types with polynomial functors. Polynomial functors form a bicategory. Polynomial functors also have a derivation on them.
The beginning of a connection was sketched by Robin Cockett in the following talk:
http://www.mathstat.dal.ca/~selinger/fmcs2012/slides/FMCS2012-Cockett2.pdf
One first has to push the development of differential categories through to the bicategory level. A precursor to differential structure is left additive structure; the talk sketches out the left additive structure on polynomial functors. The talk also goes on to discuss the derivative of polynomial functors, and points out that the chain rule may be tricky. At the end the talk concludes that there is still a bit to sort out.
