What is cosh(List(Bool))? Or beyond algebra: analysis of data types
34 points by knl
34 points by knl
Conor McBride has a collection of papers on the calculus of algebraic data types. The LICS 2001 paper has been cited a lot despite being rejected.
There was a good discussion on this topic last year.
One place where I sometimes think about “derivatives of types” is in incremental computation (think materialize, timely dataflow, etc).
It is interesting that the bag has a simple and natural derivative, and that doing incremental computation seems to work out a lot simpler with bags than with sets or lists. I suspect there is a connection!
I’d love to be able to take “derivatives” of programs. Not autodiff for real numbers, I mean “if the input of arbitrary function f changes slightly, can we recompute the new output cheapy?” as well as the followup questions “what data needs to be cached to enable this?” and “what set of data structures and operations should I provide for users to make programs with which the compiler can automatically provide cheap incremental computation?” (the latter being “materialize but for general purpose programming langauges”).
Relational operations seem most naturally implemented with bag semantics (preserving set semantics requires constant deduplication of intermediate results).
A paper I read somewhat recently is called logarithm and program testing which connects logarithms of generic types to the “smallest inputs to verify properties of polymorphic functions” in property-based testing. It’s a good read, and curious application of the algebra of data types.
This was a very nice article!
I noticed that the partial derivatives of ADTs are very similar in flavour to the derivatives of regular expressions (unsurprisingly). There was a recent post about those here: https://lobste.rs/s/ysq9w3/regular_expression_derivatives_python
who would boldly go where no series converged before and through a sequence of meaningless intermediate steps arrive to a correct result.
Loved this line!
The central rôle of e^x in analysis indicates that perhaps it is multiset, rather than list, that is the most important datastructure.
This brings to mind, at least superficially, FRACTRAN, in which the state of a register machine is identified with a multiset, which is identified with the prime factorization of a natural number.