4 ms·
No, it is a completely egotistical and futile exercise used to produce public funding consuming academics. This method of doing things offers a sound approach
by mathetic 10y ago
No, it is a completely egotistical and futile exercise used to produce public funding consuming academics.
This method of doing things offers a sound approach to developing things rather than ad-hoc implementations. It allows properties about the method to be proved with absolute certainty.
In hindsight after you have "done" it, everything seems they were doable.
Monads for example proved to be very useful in functional languages, and as Phil Wadler puts it "it is doubtful that the structuring methods presented here would have been discovered without the insight afforded by category theory. But once discovered they are easily expressed without any reference to things categorical. No knowledge of category theory is required to read these notes." in his now famous paper [0].
But maybe monads are too exotic to provide a good example. Let's talk about higher-order functions instead. Closures are very common to all programming languages these days and they existed long long before we had the first computer thanks to the lambda calculus. It would be nice then we look at lambda calculus to understand use and ramifications of such constructs. What they are good for, if they have limitations, etc.
More importantly, there seems to be a correspondent logic to useful type theories we come up with (or perhaps discover). One famous example is Curry-Howard correspondence [1]. So it might be useful if we understood what has come decades, sometimes centuries before, rather than reinventing the wheel.
[0] http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/baastad.pdf http://homepages.inf.ed.ac.uk/wadler/papers/marktoberdorf/ba...
[1] https://en.wikipedia.org/wiki/Curry–Howard_correspondence https://en.wikipedia.org/wiki/Curry–Howard_correspondence
- bassislife 10y ago> But maybe monads are too exotic to provide a good example. Nah, it's fine. But a monad is just a part of an abstraction. Which also means that they have been used without that specific denomination for ages. The use of Category theory just allows to think about things out-of-context but it is not necessary nor evident that it "always" leads to interesting results for the everyday programmer. It is like the difference between applied and pure mathematics. The concept of a monad in haskell was introduced to solve a specific problem though, if I remember well. And it was not uncontroversial. But people who know better could chime in.
- gravypod 10y agoHave there been developments of similar or better constructs accidentally/naturally outside of the efforts put forward by PLT? If I wanted to see what was being said by the field, are there any seminal works to 'ingest'?
- bassislife 10y agoFor category theory, I don't think so. But if we take tensor algebra, of course, in physics, especially quantum mechanics .The thing is, you could approach the same physical problem at different levels of abstraction and would therefore use either or. For the study of manifolds, people generally tend to favor tensorial analysis. But some results could be found within the framework of category theory. In terms of seminal work, I admit I am quite ignorant. I would check with SIAM.