Timeline for Differential categories vs McBride's notion of derivative
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 1, 2017 at 18:10 | answer | added | Jonathan Gallagher | timeline score: 2 | |
| May 4, 2016 at 8:07 | comment | added | Damiano Mazza | 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. | |
| May 2, 2016 at 22:57 | review | First posts | |||
| May 2, 2016 at 23:37 | |||||
| May 2, 2016 at 22:56 | history | asked | user278559 | CC BY-SA 3.0 |