4 ms·
Calculus already has types. The type of a function is f:R -> R. If X and Y are normed linear spaces and f:X -> Y the type of the (Frechet) derivative is Df:X
by keithalewis 4y ago
Calculus already has types. The type of a function is f:R -> R.
If X and Y are normed linear spaces and f:X -> Y the type of the (Frechet) derivative is Df:X -> L(X,Y), where L(X,Y) is the space of linear operators from X to Y.
- cvoss 4y agoThe linked discussion is actually about performing calculus-like operations on type-theory types. (A natural next step after observing the similarities between algebraic types and algebra.) It's not about imposing a type system onto traditional calculus.
- nh23423fefe 4y agopolitest RTFA
- keithalewis 4y agoI had a different read on that but I am familiar with the link to Haskell zippers. People seem to assume if someone wrote something about Haskell they must be smart. Their "derivative" of trees implicitly assumes the cartesian product A x B is isomorphic to B x A. Just like the Frechet derivative for non-commutative Banach spaces, the derivative of T^2 is not 2 T dT, it is T dT + dT T.