3 ms·

Thanks. Very informative. I actually didn't know about Backus. I just assumed because of CT all academics who study FP view FP this way. Do you have the source

Thanks. Very informative. I actually didn't know about Backus. I just assumed because of CT all academics who study FP view FP this way. Do you have the source where Backus actually talks about the stuff you mentioned?

throwaway17_17 7y ago
The canonical source for Backus is his Turing Award Lecture, which was turned into a paper, by which time he had renamed his system FFP (Formal Functional Programming). [0]. There was some longer term research into his FFP system, done by Williams and Wimmers (who gave a much loved talk titled ‘Sacrificing simplicity for convenience: Where do you draw the line?’ that I can not find a copy or transcript of to save my life in 1988) which evolved into The FL language also by Backus, with Williams and Wimmers[2]. There is a great succinct rundown of Backus’ work in this area and those who continued it in [3], it is a little lengthy so I didn’t want to just big block quote it. Also, with regard to the CT thing, I totally get that. The predominance of CT-based concepts (no matter how far they are actually removed from the mathematical background of actual CT) are one of the defining features of modern functional programming, to the point people make jokes about needing to know CT to write ‘Hello World’ in Haskell. However, and I admit to having an unhealthy obsession with following PLT academia, it really is a little bit of a smoke screen. Nearly all ‘functional’ languages are based on the lambda calculus and various augmentations thereto, and so most of the CT applied in the area tends to be refinements and imports of various constructs into some potentially BiCartesian Closed Category (which is what the lambda calculus with the common functional programming additions of product and sum types and 1st class functions is as a category). But as I said before, the fundamental construct in the computational model is application via substitution. All of the advanced categorical constructs and tools still hold for compositional languages, but, as the theory goes, you gain an algebraic theory of manipulation of the actual programming language by virtue of the categorical properties of composition (and the inferred lack of hand-wringing over the semantics of substitution. Sorry for the wall of text, this particular corner of CS and PLT is my favorite place, so any chance to talk about it I jump on. —————————————————————- 0 - https://www.thocp.net/biographies/papers/backus_turingaward_lecture.pdf https://www.thocp.net/biographies/papers/backus_turingaward_... 2 - http://citeseerx.ist.psu.edu/viewdoc/citations;jsessionid=B954240F0724D34E06A7F8334B11867E?doi=10.1.1.142.362 http://citeseerx.ist.psu.edu/viewdoc/citations;jsessionid=B9... 3 - http://joy-lang.org/papers-on-joy/joy-compared-with-other-functional-languages http://joy-lang.org/papers-on-joy/joy-compared-with-other-fu...

throwaway17_17 7y ago

The canonical source for Backus is his Turing Award Lecture, which was turned into a paper, by which time he had renamed his system FFP (Formal Functional Programming). [0]. There was some longer term research into his FFP system, done by Williams and Wimmers (who gave a much loved talk titled ‘Sacrificing simplicity for convenience: Where do you draw the line?’ that I can not find a copy or transcript of to save my life in 1988) which evolved into The FL language also by Backus, with Williams and Wimmers[2]. There is a great succinct rundown of Backus’ work in this area and those who continued it in [3], it is a little lengthy so I didn’t want to just big block quote it. Also, with regard to the CT thing, I totally get that. The predominance of CT-based concepts (no matter how far they are actually removed from the mathematical background of actual CT) are one of the defining features of modern functional programming, to the point people make jokes about needing to know CT to write ‘Hello World’ in Haskell. However, and I admit to having an unhealthy obsession with following PLT academia, it really is a little bit of a smoke screen. Nearly all ‘functional’ languages are based on the lambda calculus and various augmentations thereto, and so most of the CT applied in the area tends to be refinements and imports of various constructs into some potentially BiCartesian Closed Category (which is what the lambda calculus with the common functional programming additions of product and sum types and 1st class functions is as a category). But as I said before, the fundamental construct in the computational model is application via substitution. All of the advanced categorical constructs and tools still hold for compositional languages, but, as the theory goes, you gain an algebraic theory of manipulation of the actual programming language by virtue of the categorical properties of composition (and the inferred lack of hand-wringing over the semantics of substitution. Sorry for the wall of text, this particular corner of CS and PLT is my favorite place, so any chance to talk about it I jump on. —————————————————————- 0 - https://www.thocp.net/biographies/papers/backus_turingaward_lecture.pdf https://www.thocp.net/biographies/papers/backus_turingaward_... 2 - http://citeseerx.ist.psu.edu/viewdoc/citations;jsessionid=B954240F0724D34E06A7F8334B11867E?doi=10.1.1.142.362 http://citeseerx.ist.psu.edu/viewdoc/citations;jsessionid=B9... 3 - http://joy-lang.org/papers-on-joy/joy-compared-with-other-functional-languages http://joy-lang.org/papers-on-joy/joy-compared-with-other-fu...