4 ms·

So the algebra of data types, as described, is simply the algebra of natural numbers. I guess this can't be the whole story because it does not describe types w

So the algebra of data types, as described, is simply the algebra of natural numbers. I guess this can't be the whole story because it does not describe types which can get an infinite number of values. But still I wonder, what is the practical advantage of using this simple mathematical structure? What does it buy us? Not trying to be snarky, I just don't see the point.

crntaylor 14y ago
Indeed, it's not the whole story. Infinite types and recursive types will come along in part 2! As to the practical advantage - does there have to be one? Isn't the fact that it's intellectually gratifying enough? If you insist, though - I sometimes see the kind of laws I presented used in actual Haskell code. For example, in the Data.Lens package[0] you can consider a lens on a a structure of type a to be composed of a getter and a setter of values of type b data Lens a b = Lens (a -> b, a -> b -> a) which is refactored, using the law (a -> b, a -> c) == a -> (b,c), to look like data Lens a b = Lens (a -> (b, b -> a)) which allows for a more efficient 'modify' operation. It also allows you to notice that lenses are related to the 'Store' comonad[1]: data Store b a = Store (b, b -> a) data Lens a b = Lens (a -> Store b a) on which a lot of the Data.Lens internals are based. [0] https://github.com/ekmett/lens https://github.com/ekmett/lens [1] http://stackoverflow.com/questions/8766246/what-is-the-store-comonad http://stackoverflow.com/questions/8766246/what-is-the-store...
- guygurari 14y ago
  Thanks for explaining and for the examples. I would like to clarify that by 'practical advantage' I do not mean 'how does this help us write a web app' (although that would be nice), I mean 'how does this help us better understand programming'. In my experience, if you find that a problem admits a mathematical structure, but the structure is very simple, then often the structure does not lead to interesting insights -- it is just a form of taxonomy. This happens for example in my field (theoretical physics), where some objects can be described in fancy ways using category theory. These descriptions do not lead to any practical results, like discovering new mathematical properties of the objects involved. Personally I do not find these descriptions gratifying because, again, they are just taxonomy. There usually needs to be some minimal amount of mathematical structure (like group structure, manifold structure, etc.) in order to be able to say something new and non-trivial about the problem at hand.
  - crntaylor 14y ago
    Does it help if I tell you that types form a semiring[0]? Note that the natural numbers also form a semiring (with 0 as the additive identity and 1 as the multiplicative identity). The natural numbers can be embedded in the semiring of types, but they are a strict subset - there are types that don't correspond to natural numbers (which addressed the point on the great-grandparent post). There's a great paper by Fiore and Leinster[1] called "Objects of Categories as Complex Numbers" which shows how you can treat elements of some semirings as complex numbers for the purposes of proving arithmetic statements about them, and then convert the proofs that use complex numbers into valid proofs in the semiring. [0] http://en.wikipedia.org/wiki/Semiring http://en.wikipedia.org/wiki/Semiring [1] http://arxiv.org/abs/math/0212377 http://arxiv.org/abs/math/0212377
tikhonj 14y ago
A fun example is zippers. A zipper over some structure is a purely functional way to keep track of your "position" inside the structure, which ideally lets you move around it easily. Normally, when we use lists, we do something to the head and recurse on the tail. This allows us to easily move forwards through the list, but what if we sometimes want to go backwards? It's very easy to come up with a structure that lets us do this: we just keep track of the previous elements of the list as well as the remaining ones. This is exactly what a zipper over a list is: zipper [a] <=> ([a], [a]) So if we have the list [1,2,3,4], the zipper would let us represent [1,2,^3,4] where ^ is our position; it would look something like ([2, 1], [3, 4]). We could then move forwards to ([3,2,1], [4]) or backwards to ([1], [2,3,4]). This is a very simple and elegant idea, but also very easy to come up with yourself; no need for any algebra. However, there is an interesting observation to be made: a zipper corresponds to the derivative of a type! I think crntaylor is going to cover the mechanics of this in a future post. This gives us a couple of useful insights. For one, it means we can apply the derivative operation repeatedly to get as many "cursors" into our type as we want. We could have a zipper with two positions in the list, or three positions in the list, or whatever. Additionally, it also tells us how to generalize zippers to other types like trees. At least to me, this is not obvious and the algebra really helps here. So we can go from the very simple structure of using ([a], [a]) to represent a position in [a] to having an arbitrary number of positions in arbitrary types like trees. I think that's pretty cool. Another fun example is packing seven binary trees into one, using complex numbers. This is a bit more involved, so I'll let much better writers than me cover it: there's the original paper[1] as well as a nice blog post[2] about it. I think it's a very cool demonstration of how this sort of algebraic reasoning can be useful even with a fairly trivial algebraic structure. [1]: http://www.cs.toronto.edu/~yuvalf/7trees.pdf http://www.cs.toronto.edu/~yuvalf/7trees.pdf [2]: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nuclear.html http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu... Also, recognizing this sort of structure can help us organize our programs. Often, even trivial abstractions are useful just for organizing code even if you don't get any especial insight from them. For example, monoids are very trivial, but are extremely useful for writing libraries. Also, I think this is exactly the sort of abstraction which would make writing generic programs much easier, but I do not know enough about generic programming to be sure. (Here it's "generic" in the Haskell sense--programs that operate based on a type's structure and apply to many different types rather than generic in the Java sense, which is just parametric polymorphism.) Just something else to look into if you're curious.
jfarmer 14y ago
I started programming in high school as a hobby and went on to study mathematics and linguistics at the University of Chicago, where I graduated in 2006. The date is just to give a sense of the timeline: it wasn't until 2-3 years ago that these worlds felt meaningfully compatible to me. So, I'll do my best to explain why this is "practical," as someone who spent a long time trying to establish a relationship between "mathematician jfarmer" and "programmer jfarmer." For me, the #1 practical benefit is clarity. For example, you say that "the algebra of data types, as described, is simply the algebra of natural numbers." Is this really true? The mathematician's move would be to abstract out this common "algebra" and isolate that structure and that structure alone. The algebra of data types and the algebra of the natural numbers then become instances of this more universal algebra. In other words, the picture you have is that "A is an instance of B" of really it's that A and B are instances some third thing, C, that isolates their shared algebraic structure. If you're curious, the shared algebraic structure is called a semiring (http://en.wikipedia.org/wiki/Semiring http://en.wikipedia.org/wiki/Semiring). Why is this helpful? Because it makes for clearer explanations. We can understand what facts/theorems are true because of this shared structure vs. what is true because of the particularities of one of the more specific structures. We can prove things about semirings per se which will be true for any particular semiring. We then have a new strategy available to us: if we can show some structure is a semiring, a whole universe of facts become available to us without any additional work. Moreover, from this perspective, whole classes of seemingly-distinct algorithms become instances of a more abstract algorithm depending on which semiring we're operating over. For example, the probabalistic and and non-probabalistic versions of a CKY parser are instance of the same algorithm which vary only according to which semiring they're executed over. ({TRUE, FALSE}, OR, AND) and ([0,∞), +, * ), respectively. That's not just a curiosity; it's an entirely new axis of thought that reveals connections between what previously seemed like similar-but-unrelated pieces of software. It opens up the possibility of writing a function that takes a semiring specification* as input and returns a function for the "instantiated" algorithm over that semiring. * : This example requires more than just a semiring, but I'm just trying to illustrate the point.

crntaylor 14y ago

Indeed, it's not the whole story. Infinite types and recursive types will come along in part 2! As to the practical advantage - does there have to be one? Isn't the fact that it's intellectually gratifying enough? If you insist, though - I sometimes see the kind of laws I presented used in actual Haskell code. For example, in the Data.Lens package[0] you can consider a lens on a a structure of type a to be composed of a getter and a setter of values of type b data Lens a b = Lens (a -> b, a -> b -> a) which is refactored, using the law (a -> b, a -> c) == a -> (b,c), to look like data Lens a b = Lens (a -> (b, b -> a)) which allows for a more efficient 'modify' operation. It also allows you to notice that lenses are related to the 'Store' comonad[1]: data Store b a = Store (b, b -> a) data Lens a b = Lens (a -> Store b a) on which a lot of the Data.Lens internals are based. [0] https://github.com/ekmett/lens https://github.com/ekmett/lens [1] http://stackoverflow.com/questions/8766246/what-is-the-store-comonad http://stackoverflow.com/questions/8766246/what-is-the-store...

guygurari 14y ago
Thanks for explaining and for the examples. I would like to clarify that by 'practical advantage' I do not mean 'how does this help us write a web app' (although that would be nice), I mean 'how does this help us better understand programming'. In my experience, if you find that a problem admits a mathematical structure, but the structure is very simple, then often the structure does not lead to interesting insights -- it is just a form of taxonomy. This happens for example in my field (theoretical physics), where some objects can be described in fancy ways using category theory. These descriptions do not lead to any practical results, like discovering new mathematical properties of the objects involved. Personally I do not find these descriptions gratifying because, again, they are just taxonomy. There usually needs to be some minimal amount of mathematical structure (like group structure, manifold structure, etc.) in order to be able to say something new and non-trivial about the problem at hand.
- crntaylor 14y ago
  Does it help if I tell you that types form a semiring[0]? Note that the natural numbers also form a semiring (with 0 as the additive identity and 1 as the multiplicative identity). The natural numbers can be embedded in the semiring of types, but they are a strict subset - there are types that don't correspond to natural numbers (which addressed the point on the great-grandparent post). There's a great paper by Fiore and Leinster[1] called "Objects of Categories as Complex Numbers" which shows how you can treat elements of some semirings as complex numbers for the purposes of proving arithmetic statements about them, and then convert the proofs that use complex numbers into valid proofs in the semiring. [0] http://en.wikipedia.org/wiki/Semiring http://en.wikipedia.org/wiki/Semiring [1] http://arxiv.org/abs/math/0212377 http://arxiv.org/abs/math/0212377

tikhonj 14y ago

A fun example is zippers. A zipper over some structure is a purely functional way to keep track of your "position" inside the structure, which ideally lets you move around it easily. Normally, when we use lists, we do something to the head and recurse on the tail. This allows us to easily move forwards through the list, but what if we sometimes want to go backwards? It's very easy to come up with a structure that lets us do this: we just keep track of the previous elements of the list as well as the remaining ones. This is exactly what a zipper over a list is: zipper [a] <=> ([a], [a]) So if we have the list [1,2,3,4], the zipper would let us represent [1,2,^3,4] where ^ is our position; it would look something like ([2, 1], [3, 4]). We could then move forwards to ([3,2,1], [4]) or backwards to ([1], [2,3,4]). This is a very simple and elegant idea, but also very easy to come up with yourself; no need for any algebra. However, there is an interesting observation to be made: a zipper corresponds to the derivative of a type! I think crntaylor is going to cover the mechanics of this in a future post. This gives us a couple of useful insights. For one, it means we can apply the derivative operation repeatedly to get as many "cursors" into our type as we want. We could have a zipper with two positions in the list, or three positions in the list, or whatever. Additionally, it also tells us how to generalize zippers to other types like trees. At least to me, this is not obvious and the algebra really helps here. So we can go from the very simple structure of using ([a], [a]) to represent a position in [a] to having an arbitrary number of positions in arbitrary types like trees. I think that's pretty cool. Another fun example is packing seven binary trees into one, using complex numbers. This is a bit more involved, so I'll let much better writers than me cover it: there's the original paper[1] as well as a nice blog post[2] about it. I think it's a very cool demonstration of how this sort of algebraic reasoning can be useful even with a fairly trivial algebraic structure. [1]: http://www.cs.toronto.edu/~yuvalf/7trees.pdf http://www.cs.toronto.edu/~yuvalf/7trees.pdf [2]: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nuclear.html http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu... Also, recognizing this sort of structure can help us organize our programs. Often, even trivial abstractions are useful just for organizing code even if you don't get any especial insight from them. For example, monoids are very trivial, but are extremely useful for writing libraries. Also, I think this is exactly the sort of abstraction which would make writing generic programs much easier, but I do not know enough about generic programming to be sure. (Here it's "generic" in the Haskell sense--programs that operate based on a type's structure and apply to many different types rather than generic in the Java sense, which is just parametric polymorphism.) Just something else to look into if you're curious.

jfarmer 14y ago

I started programming in high school as a hobby and went on to study mathematics and linguistics at the University of Chicago, where I graduated in 2006. The date is just to give a sense of the timeline: it wasn't until 2-3 years ago that these worlds felt meaningfully compatible to me. So, I'll do my best to explain why this is "practical," as someone who spent a long time trying to establish a relationship between "mathematician jfarmer" and "programmer jfarmer." For me, the #1 practical benefit is clarity. For example, you say that "the algebra of data types, as described, is simply the algebra of natural numbers." Is this really true? The mathematician's move would be to abstract out this common "algebra" and isolate that structure and that structure alone. The algebra of data types and the algebra of the natural numbers then become instances of this more universal algebra. In other words, the picture you have is that "A is an instance of B" of really it's that A and B are instances some third thing, C, that isolates their shared algebraic structure. If you're curious, the shared algebraic structure is called a semiring (http://en.wikipedia.org/wiki/Semiring http://en.wikipedia.org/wiki/Semiring). Why is this helpful? Because it makes for clearer explanations. We can understand what facts/theorems are true because of this shared structure vs. what is true because of the particularities of one of the more specific structures. We can prove things about semirings per se which will be true for any particular semiring. We then have a new strategy available to us: if we can show some structure is a semiring, a whole universe of facts become available to us without any additional work. Moreover, from this perspective, whole classes of seemingly-distinct algorithms become instances of a more abstract algorithm depending on which semiring we're operating over. For example, the probabalistic and and non-probabalistic versions of a CKY parser are instance of the same algorithm which vary only according to which semiring they're executed over. ({TRUE, FALSE}, OR, AND) and ([0,∞), +, * ), respectively. That's not just a curiosity; it's an entirely new axis of thought that reveals connections between what previously seemed like similar-but-unrelated pieces of software. It opens up the possibility of writing a function that takes a semiring specification* as input and returns a function for the "instantiated" algorithm over that semiring. * : This example requires more than just a semiring, but I'm just trying to illustrate the point.