[HN Gopher] Taking the derivative of an algebraic data type [pdf]
___________________________________________________________________
Taking the derivative of an algebraic data type [pdf]
Author : pxeger1
Score : 56 points
Date : 2023-01-12 18:59 UTC (4 hours ago)
(HTM) web link (strictlypositive.org)
(TXT) w3m dump (strictlypositive.org)
| sampo wrote:
| This unpublished manuscript was published in 2001, according to
| Google Scholar.
| chobytes wrote:
| The concept of a derivation on types could be interesting... but
| the notation is a bit much for me.
|
| Differential fields are (as I understand it) a hot topic at the
| moment. Maybe there is some interesting crossovers.
| mjfl wrote:
| For the derivative, shouldn't there be some notion of continuum,
| of a limiting process to define a slope at a particular point?
| Otherwise this is just a delta is it not?
| chobytes wrote:
| There is a general notion of derivations I believe theyre
| using. Ie anything that obeys the Leibniz rule (fg)' = f'g+fh'.
|
| Its an informative exercise to see how many of the standard
| rules of calculus can be derived using just this rule.
| enricozb wrote:
| Some related links (specifically that they perform "high school"
| algebra on types):
|
| - Seven trees in one [0], a paper showing a bijection between
| binary trees and seven-tuples of binary trees.
|
| - The algebra of algebraic data types [1] discusses Taylor
| expansions of data types.
|
| - Differentiation of higher-order types [2] is commenting on OP's
| paper.
|
| I used to be really interested in type theory, but haven't had as
| much time to explore it, but over the years I've saved these
| links (and the one posted).
|
| [0]: https://arxiv.org/pdf/math/9405205.pdf
|
| [1]: https://codewords.recurse.com/issues/three/algebra-and-
| calcu...
|
| [2]: http://conal.net/blog/posts/differentiation-of-higher-
| order-...
| danbruc wrote:
| _Seven trees in one [0], a paper showing a bijection between
| binary trees and seven-tuples of binary trees._
|
| Is this a surprising result? I am not quite interested enough
| to read through the paper in order to find out. Naively I would
| say, sounds maybe a bit fiddly, could have a clever trick to do
| elegantly, but does not sound too surprising or hard.
|
| Build a complete binary tree with six nodes and attach the
| seven trees from the tuple as children. This is not a
| bijections as trees without the complete tree do not map back
| into any tuple of trees, so fiddle a bit with those six nodes
| to encode some special tuples or classes of tuples. Okay, now
| you have a new problem, two encodings for some tuples, so we
| have to also fiddle a bit with the trees before attaching them.
| Yeah, that could get fiddly...
| chobytes wrote:
| Maybe Schroder-Bernstein could simplify. Easier to write 2
| injections.
| danbruc wrote:
| But from reading the first bit of the paper I think they
| are talking about something stronger, not any bijection but
| one that only requires inspecting and manipulating a
| bounded number of layers of the trees.
| mxkopy wrote:
| Something that I've found interesting is that the domain of a
| derivative always seems to be phrased in terms of open sets, even
| when the original function is defined on a closed set. It's like
| taking the derivative removes exactly the bounds from the domain.
| I wonder if one-hole contexts are to blame for that.
| hgsgm wrote:
| No, because in discrete differentiation like this, there is no
| limiting process where openness matters, and open/closedness is
| completely trivial in discrete spaces.
|
| The "one-hole" is in the discrete _types_ , not the potentially
| continuous _values_.
| auggierose wrote:
| If you want to take the derivative from all directions, the
| domain must be open. That's probably all there is to it.
| chobytes wrote:
| Can you give an example of what you mean?
| mxkopy wrote:
| https://math.stackexchange.com/questions/469735/why-is-
| diffe...
| chobytes wrote:
| Ah, I think I see. Open sets are just how we encode
| information topologically. Theyre sort of the "atoms" of
| topology; the types of opens sets you have say how the
| topology behaves.
|
| In particular open sets are neighborhoods of all of the
| points they contain. This means they contain all the
| topological information about all of their points.
|
| Closed sets are not neighborhoods of their points in
| general. Eg [0,1] contains no neighborhood of 0 or 1. Then
| we would require knowledge of the space around those points
| to know how a function behaves just on [0,1].
|
| In standard calculus this amounts to "taking the left and
| right limits".
|
| Does that help?
| _dwt wrote:
| I think lenses/optics have stolen some of zippers' (very
| localized) thunder in recent years, but I still enjoy finding
| excuses to use them every once in a while. (OK, so really just a
| couple Advent of Code problems.)
|
| I have never actually had the wherewithal to go through the whole
| automatic-derivation-of-zippers thing, but this
| (https://stackoverflow.com/questions/25554062/zipper-comonads...)
| StackOverflow Q&A (along with all of Conor McBride's SO answers -
| compiled at https://personal.cis.strath.ac.uk/conor.mcbride/so-
| pigworker...) might be of interest in conjunction with the linked
| paper.
| anon291 wrote:
| Now take the derivative of a delimited continuation.
| adamgordonbell wrote:
| Slightly related but, Jimmy Koppel teaches 'Algebriac
| Refactoring' where you use tricks from factoring polynomials
| applied to the type level of functions to yield better designs.
| It's super cool stuff.
| samvher wrote:
| Any link you could share to check this out? Quick search leads
| to a youtube video of his, but the audio is so bad it's
| unwatchable (to me at least), maybe there is something better
| out there?
| adamgordonbell wrote:
| Sorry, it was part of his software training. Not seeing a
| public version out there. Maybe he'll jump in with a link
| I've missed.
| ogogmad wrote:
| Related and useful to know:
| https://en.wikipedia.org/wiki/Combinatorial_species
|
| Also: https://en.wikipedia.org/wiki/Brzozowski_derivative
|
| Good to know about these:
| https://en.wikipedia.org/wiki/Dual_number
|
| Seems comprehensive: https://semantic-
| domain.blogspot.com/2021/02/five-and-half-d...
| wendyshu wrote:
| Similarly
| https://en.wikipedia.org/wiki/Symbolic_method_(combinatorics...
| pixelpoet wrote:
| I like the bit at the end giving credit to trains:
|
| > I feel very lucky to have stumbled on this interpretation of
| differentiation for datatypes with such potential for both
| utility and fascination, and has been intriguing me since the day
| I made the connection (whilst changing trains at Shrewsbury).
| This work has benefited greatly from hours spent on trains, [...]
| dunham wrote:
| My favorite is from Bob Atkey's Quantitative Type Theory paper:
|
| > This work is dedicated to Orwell the dog. Orwell was a good
| dog and knew well the difference between zero, one, and many
|
| https://bentnib.org/quantitative-type-theory.pdf
|
| (zero, one, many was the ring that the paper used.)
___________________________________________________________________
(page generated 2023-01-12 23:00 UTC)