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).
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...
It's definitely surprising, for a couple of reasons:
1. It isn't just the uninteresting result that the set of trees has the same cardinality as the set of 7-tuples of trees; the bijection here is given by a finite, non-looping program built out of `isEmpty : Tree -> Bool`, `getLeft : Tree -> Maybe Tree`, `getRight : Tree -> Maybe Tree`, and the constructors `empty : Tree` and `join : Tree x Tree -> Tree`
2. It isn't true for any number 1 < x < 7
3. In any case, why should it work out exactly? Why not "one tree can be encoded into seven trees, or one of these 13 remaining cases"?
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 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, [...]
I’m so bummed that I can’t understand this paper, coming from the lisp camp. Do I need to go to conferences or something to understand this? I read “learn you a Haskell” but this seems to be a bit beyond that. I can’t tell if the concept of “derivative of a type” is an overload of calculus operators (totally fine) and there’s no actual relationship or if this is a serious suggestion of a “derivative”. Huge fan of ADTs, though, great way to write composable code, so if anyone has some insight on how to get some insight, I’d love to hear it!
To give you an example: the zipper of a list is two lists - one for the elements after the current one (the hole), another for the elements before the current one, plus the current element.
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.
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?
Reminds me of this beautiful 1964 paper by Janus Brzozowski where he applies differential calculus rules symbolically to regular expressions to derive a recogniser for it.
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?
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.
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.
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-...
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...
It's definitely surprising, for a couple of reasons: 1. It isn't just the uninteresting result that the set of trees has the same cardinality as the set of 7-tuples of trees; the bijection here is given by a finite, non-looping program built out of `isEmpty : Tree -> Bool`, `getLeft : Tree -> Maybe Tree`, `getRight : Tree -> Maybe Tree`, and the constructors `empty : Tree` and `join : Tree x Tree -> Tree` 2. It isn't true for any number 1 < x < 7 3. In any case, why should it work out exactly? Why not "one tree can be encoded into seven trees, or one of these 13 remaining cases"?
The paper is quite good, but Dan Piponi has a great blog post that recasts the isomorphism as a game of "nuclear pennies", which is a fun puzzle to work out yourself: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu...
3 replies →
Maybe Schroder-Bernstein could simplify. Easier to write 2 injections.
3 replies →
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...
Similarly https://en.wikipedia.org/wiki/Symbolic_method_(combinatorics...
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.
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, [...]
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.)
I’m so bummed that I can’t understand this paper, coming from the lisp camp. Do I need to go to conferences or something to understand this? I read “learn you a Haskell” but this seems to be a bit beyond that. I can’t tell if the concept of “derivative of a type” is an overload of calculus operators (totally fine) and there’s no actual relationship or if this is a serious suggestion of a “derivative”. Huge fan of ADTs, though, great way to write composable code, so if anyone has some insight on how to get some insight, I’d love to hear it!
Maybe with some examples:
https://wiki.haskell.org/Zipper
https://en.m.wikipedia.org/wiki/Zipper_(data_structure)
To give you an example: the zipper of a list is two lists - one for the elements after the current one (the hole), another for the elements before the current one, plus the current element.
Hey sorry this is late but thank you so much! The paper on zippers was especially helpful.
The Erlang version might be more familiar to you https://ferd.ca/yet-another-article-on-zippers.html?
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.
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?
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.
1 reply →
Reminds me of this beautiful 1964 paper by Janus Brzozowski where he applies differential calculus rules symbolically to regular expressions to derive a recogniser for it.
https://dl.acm.org/doi/pdf/10.1145/321239.321249
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?
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.
https://en.wikipedia.org/wiki/Derivation_(differential_algeb... is probably what you were referring to.
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.
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.
Right, the "elements of x" made me think values, but those elements really are other types.
Crazy where operator overloading will get you. If there are postmodern math papers I feel like this is one of them
If you want to take the derivative from all directions, the domain must be open. That's probably all there is to it.
Can you give an example of what you mean?
https://math.stackexchange.com/questions/469735/why-is-diffe...
2 replies →
Now take the derivative of a delimited continuation.
This unpublished manuscript was published in 2001, according to Google Scholar.
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.
wtf?
> Clearly it’s equivalent to Choice’s use of a boolean tag. Isn’t it remarkable that algebraic manipulations agree with our intuition?
no, thats not interestimg at all. It is literally just encoding left/right in a bool.
that page seems to be doing "calculus" not on the sets but the sizes of the sets. entirely uninteresting and boring.
Haskel: making the easy stuff hard.