3 ms·

It's basically a certain kind of documentation of design patterns in programming languages. PLT emphasizes the use of formal logic and mathematics. It focuses o

by rntz 10y ago

It's basically a certain kind of documentation of design patterns in programming languages. PLT emphasizes the use of formal logic and mathematics. It focuses on systems that can be rigorously defined, and theorems that can be proven about them; as opposed to software engineering, which focuses on the issues and patterns that crop up in the practice of developing software, or HCI, which focuses on human factors. Of course, all of these are overly broad generalizations, and it's not as if there aren't points of intersection between these different ways of looking at programming languages. But the kind of stuff you'll see in a book like Types and Programming Languages is super-different in approach from the kind of stuff you'd see in, say, the Gang of Four book, both of which are different again from Bret Victor's approach.

gravypod 10y ago
Are there any benefits or contributions made by this method that couldn't be simply done by "doing" it. IE: Implement a language and use that as an example and improve it.
- 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 ago
      Have 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 ago
        For 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.
seanmcdirmid 10y ago
> It's basically a certain kind of documentation of design patterns in programming languages. PLT has become its own thing, and work in the area is not necessarily related to PL. If you scan current papers at POPL, you'll see a trend of applying language-oriented theory to problem X where X has nothing to do with implementing/designing a programming language. We can apply theory to PL, but many of the factors in a PL design today (or yesterday) are not rooted in theory. > But the kind of stuff you'll see in a book like Types and Programming Languages is super-different in approach from the kind of stuff you'd see in, say, the Gang of Four book, both of which are different again from Bret Victor's approach. It is not even just the approach that is different, but the goals and outcomes.
- gravypod 10y ago
  Would you mind describing some of the goals, current problems, and some "must-read" papers on the topic? I'm in a university so I have access to most journals. I'm very interested in learning more about this.
  - seanmcdirmid 10y ago
    PL is vastly huge, so you have to be more specific about "topic." What are you interested in learning? I personally specialize in experience, and could list many (what I consider seminal) papers that are not even on the radar for other PL researchers.

by rntz 10y ago

gravypod 10y ago

Are there any benefits or contributions made by this method that couldn't be simply done by "doing" it. IE: Implement a language and use that as an example and improve it.

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 ago
    Have 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 ago
      For 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.

seanmcdirmid 10y ago

> It's basically a certain kind of documentation of design patterns in programming languages. PLT has become its own thing, and work in the area is not necessarily related to PL. If you scan current papers at POPL, you'll see a trend of applying language-oriented theory to problem X where X has nothing to do with implementing/designing a programming language. We can apply theory to PL, but many of the factors in a PL design today (or yesterday) are not rooted in theory. > But the kind of stuff you'll see in a book like Types and Programming Languages is super-different in approach from the kind of stuff you'd see in, say, the Gang of Four book, both of which are different again from Bret Victor's approach. It is not even just the approach that is different, but the goals and outcomes.

gravypod 10y ago
Would you mind describing some of the goals, current problems, and some "must-read" papers on the topic? I'm in a university so I have access to most journals. I'm very interested in learning more about this.
- seanmcdirmid 10y ago
  PL is vastly huge, so you have to be more specific about "topic." What are you interested in learning? I personally specialize in experience, and could list many (what I consider seminal) papers that are not even on the radar for other PL researchers.