2 ms·

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'

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

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