The derivative of a Regular Type is its Type of One-Hole Context

This is a surprising computational application related to Qiaochu's example, but different enough to warrant some explanation. Apologies for some of my hand-waveyness.

In a suitably pure programming language (like Haskell) we can think of data types as being objects of a category and functions (suitably qualified) as arrows. We often want to build one type from another. For example, given a type $X$ we can form the type $X\times X$, the type of pairs of $X$'s. Similarly we can form coproducts which correspond to objects that can be of one type or another. Eg. if $Y=X+X^2$ then $Y$ is a type which contains either an $X$ or a pair of $X$'s. The functions that construct one type from another, call them type constructors, can naturally be thought of as functors. So $P$ defined by $P(X)=X^2$ is a functor. If $(x,y)$ is in $X^2$ then $Pf(x,y)=(f(x),f(y))$. Types form a semiring.

Sometimes we want to make a 'hole' in a type constructors. If $F$ is a type constructor, then $F(A)$ can be thought of as a container of elements of type $A$. An "$F$ with a hole in it" is one of these containers but with one of its elements removed, but still keeping information about where the element was removed from. For example consider $F(X)=X^3$. $F$ makes triples of $X$'s. A triple with a hole in it consists of just two $X$'s as well as enough information to tell where the third element was removed from. There are just three places it could have come from, so we can describe the removal site using a type with just three elements. Call it $3$. So a triple with a hole in it is a pair consisting of an element of type $3$ and an element of type $X^2$. Ie. $3X^2$. This is $F'(X)$.

This works more generally. We make holes in type constructors by differentiating them.

It even works with recursive types. For example, a list of $X$'s is, by definition, either the empty list, or a pair consisting of an $X$ and a list. We have an equation

$L(X)=1+XL(X)$.

We can differentiate this to get

$L'(X)=L(X)+XL'(X)$

This gives a recursive equation for a type of a list with a hole in it. This is in fact an example of a type called a zipper. Used in many places such as this application.

(Much of this applies in the category $Set$ but the recursive equations can introduce some issues of well-foundedness if taken too literally.)

Many of the usual properties of derivatives acquire straightforward computational interpretations: linearity, the product rule, the chain rule, even the Faà di Bruno formula.

Anyway, check out the paper which has none of the errors I've probably introduced.

(Curiously, you can also make sense of finite differences of types even though we only have a semiring and don't have subtraction of types.)

The derivative of a Regular Type is its Type of One-Hole Context

This is a surprising computational application related to Qiaochu's example, but different enough to warrant some explanation. Apologies for some of my hand-waveyness.

In a suitably pure programming language (like Haskell) we can think of data types as being objects of a category and functions (suitably qualified) as arrows. We often want to build one type from another. For example, given a type $X$ we can form the type $X\times X$, the type of pairs of $X$'s. Similarly we can form coproducts which correspond to objects that can be of one type or another. Eg. if $Y=X+X^2$ then $Y$ is a type which contains either an $X$ or a pair of $X$'s. The functions that construct one type from another, call them type constructors, can naturally be thought of as functors. So $P$ defined by $P(X)=X^2$ is a functor. If $(x,y)$ is in $X^2$ then $Pf(x,y)=(f(x),f(y))$. Types form a semiring.

Sometimes we want to make a 'hole' in a type constructors. If $F$ is a type constructor, then $F(A)$ can be thought of as a container of elements of type $A$. An "$F$ with a hole in it" is one of these containers but with one of its elements removed, but still keeping information about where the element was removed from. For example consider $F(X)=X^3$. $F$ makes triples of $X$'s. A triple with a hole in it consists of just two $X$'s as well as enough information to tell where the third element was removed from. There are just three places it could have come from, so we can describe the removal site using a type with just three elements. Call it $3$. So a triple with a hole in it is a pair consisting of an element of type $3$ and an element of type $X^2$. Ie. $3X^2$. This is $F'(X)$.

This works more generally. We make holes in type constructors by differentiating them.

It even works with recursive types. For example, a list of $X$'s is, by definition, either the empty list, or a pair consisting of an $X$ and a list. We have an equation

$L(X)=1+XL(X)$.

We can differentiate this to get

$L'(X)=L(X)+XL'(X)$

This gives a recursive equation for a type of a list with a hole in it. This is in fact an example of a type called a zipper. Used in many places such as this application. In the particular case of lists $L'(X)$ defines a pair of lists of $X$'s.

(Much of this applies in the category $Set$ but the recursive equations can introduce some issues of well-foundedness if taken too literally.)

Many of the usual properties of derivatives acquire straightforward computational interpretations: linearity, the product rule, the chain rule, even the Faà di Bruno formula.

Anyway, check out the papers which have none of the errors I've probably introduced. There's also a close relationship with combinatorial species.

(Curiously, you can also make sense of finite differences of types even though we only have a semiring and don't have subtraction of types.)

The derivative of a Regular Type is its Type of One-Hole Context

This is a surprising computational application related to Qiaochu's example, but different enough to warrant some explanation. Apologies for some of my hand-waveyness.

In a suitably pure programming language (like Haskell) we can think of data types as being objects of a category and functions (suitably qualified) as arrows. We often want to build one type from another. For example, given a type $X$ we can form the type $X\times X$, the type of pairs of $X$'s. Similarly we can form coproducts which correspond to objects that can be of one type or another. Eg. if $Y=X+X^2$ then $Y$ is a type which contains either an $X$ or a pair of $X$'s. The functions that construct one type from another, call them type constructors, can naturally be thought of as functors. So $P$ defined by $P(X)=X^2$ is a functor. If $(x,y)$ is in $X^2$ then $Pf(x,y)=(f(x),f(y))$. Types form a semiring.

Sometimes we want to make a 'hole' in a type constructors. If $F$ is a type constructor, then $F(A)$ can be thought of as a container of elements of type $A$. An "$F$ with a hole in it" is one of these containers but with one of its elements removed, but still keeping information about where the element was removed from. For example consider $F(X)=X^3$. $F$ makes triples of $X$'s. A triple with a hole in it consists of just two $X$'s as well as enough information to tell where the third element was removed from. There are just three places it could have come from, so we can describe the removal site using a type with just three elements. Call it $3$. So a triple with a hole in it is a pair consisting of an element of type $3$ and an element of type $X^2$. Ie. $3X^2$. This is $F'(X)$.

This works more generally. We make holes in type constructors by differentiating them.

It even works with recursive types. For example, a list of $X$'s is, by definition, either the empty list, or a pair consisting of an $X$ and a list. We have an equation

$L(X)=1+XL(X)$.

We can differentiate this to get

$L'(X)=L(X)+XL'(X)$

This gives a recursive equation for a type of a list with a hole in it. This is in fact an example of a type called a zipper. Used in many places such as this application.

(Much of this applies in the category $Set$ but the recursive equations can introduce some issues of well-foundedness if taken too literally.)

Anyway, check out the paper which has none of the errors I've probably introduced.

(Curiously, you can also make sense of finite differences of types even though we only have a semiring and don't have subtraction of types.)

The derivative of a Regular Type is its Type of One-Hole Context

This is a surprising computational application related to Qiaochu's example, but different enough to warrant some explanation. Apologies for some of my hand-waveyness.

In a suitably pure programming language (like Haskell) we can think of data types as being objects of a category and functions (suitably qualified) as arrows. We often want to build one type from another. For example, given a type $X$ we can form the type $X\times X$, the type of pairs of $X$'s. Similarly we can form coproducts which correspond to objects that can be of one type or another. Eg. if $Y=X+X^2$ then $Y$ is a type which contains either an $X$ or a pair of $X$'s. The functions that construct one type from another, call them type constructors, can naturally be thought of as functors. So $P$ defined by $P(X)=X^2$ is a functor. If $(x,y)$ is in $X^2$ then $Pf(x,y)=(f(x),f(y))$. Types form a semiring.

Sometimes we want to make a 'hole' in a type constructors. If $F$ is a type constructor, then $F(A)$ can be thought of as a container of elements of type $A$. An "$F$ with a hole in it" is one of these containers but with one of its elements removed, but still keeping information about where the element was removed from. For example consider $F(X)=X^3$. $F$ makes triples of $X$'s. A triple with a hole in it consists of just two $X$'s as well as enough information to tell where the third element was removed from. There are just three places it could have come from, so we can describe the removal site using a type with just three elements. Call it $3$. So a triple with a hole in it is a pair consisting of an element of type $3$ and an element of type $X^2$. Ie. $3X^2$. This is $F'(X)$.

This works more generally. We make holes in type constructors by differentiating them.

It even works with recursive types. For example, a list of $X$'s is, by definition, either the empty list, or a pair consisting of an $X$ and a list. We have an equation

$L(X)=1+XL(X)$.

We can differentiate this to get

$L'(X)=L(X)+XL'(X)$

This gives a recursive equation for a type of a list with a hole in it. This is in fact an example of a type called a zipper. Used in many places such as this application.

(Much of this applies in the category $Set$ but the recursive equations can introduce some issues of well-foundedness if taken too literally.)

Many of the usual properties of derivatives acquire straightforward computational interpretations: linearity, the product rule, the chain rule, even the Faà di Bruno formula.

Anyway, check out the paper which has none of the errors I've probably introduced.

(Curiously, you can also make sense of finite differences of types even though we only have a semiring and don't have subtraction of types.)