3 ms·
HNers, let me tell what Backus finally had in mind come to fruition; I only figured this out recently: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-20
by Ericson2314 7y ago
HNers, let me tell what Backus finally had in mind come to fruition; I only figured this out recently: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-130.pdf https://www2.eecs.berkeley.edu/Pubs/TechRpts/2014/EECS-2014-...
Here's the thing, Backus was not coming from the lisp and embryonic ML communities that were function programming research at the time. This was career-retrospective speech be a new-commer to the field. I think the existing community was surprised and bemused.
Certainly your regular function programminger would have chuckled at all the "point-free" style FP. This was a decade before Haskell mind you, and at least a decade before lots of function reuse became popular (being blocked on better strictness analysis and a lack of type classes and instances). Remember in then-cutting-edge Scheme, (define ...) has an implicit (begin ...) rather than single-expression body, and don't get me started on the other imperative lisps. APL before FP just made the existing community laugh harder.
So fast forward a while, and even today implicit parallelism is not happening much in production in Haskell. Applicative is much more popular than Arrow, and thus everyone is still writing Von Neuman code even if its dressed up functionally.
Well, let me tell, that thesis puts a lot of the pieces together:
The real genius of point-free isn't getting rid of the names. We have debruign indices for that. Nor is it allowing other modules of computation. Computer scientists found good ole' 1970s Category Theory (In principle, Backus could have done this too!) and now we know about (symmetric) monoidal categories and their internal languages and all the stuff we need to point-free-ify the programs in lambda-calculus-influenced calculii.
The real genius is dealing with dynamism / higher-order programs. With the raw lambda calculus, you are in a fun house of higher-orderism and it's hard to jump out of the substitution / term-rewritting mindset. CPS, which occupied much of the functional research community for at least a man-decade, only further serializes and higher-order-ifizes things. Monadic programs bind promiscuously; every step is potentially dynamic af, one again also serializing and higher-order-ifizing things.
With arrow-like things, however (and Control.Cateogry.* and Profunctor is really much better at distilling the concepts than the legacy Arrow class, thanks Ed), suddenly we have a decently expressive form of computation with no lambdas in site. We've lifted the "fog of war", freeing the first order "90%" of the work from the higher order "10%".
Arrow notation as implemented in Haskell today, however, abuses `arr` for the structural rules of the guest language (weakening, contraction, and exchange per Wikipedia [1]). This reshrowds everything and ruins all the promise of Arrows. Yuck.
Back to the thesis, there are 2 big contributions:
1) A practical version of Arrow which doesn't need arr for structural rules. (Control.Cateogry.* since does this better and with more faithfulness to the math, but had to start somewhere.)
2) A theory of heterogenous metaprogramming so the first order and higher order bits don't even have to be the same language. We're talking things like and FPGA that computes its own re-flashing.
There is also a protoype implementation of various lambdas so humans can still use names, but I hear its bitrotted and so I can't vouch for it.
So, back to John Backus. The thing is programmers are lazy. They rather write in the language they know, or learn the language their teachers know. Also, humans need at least the option of some names (even if we have to name too many things today), so mandatory combinators will cause problems as long as we struck programming in shitty, 1-dimentional text. Finally, without at least the taste of actually compiling to other programming models, along with scaling programs with the Von Neumann model, the economic and curiosity incentives just aren't there. And in 1978 the Von Neuman model was still fucking killing it. Wires were fast, and components be they spinning disks, ALUs, or DRAM were all kinda slow but in similar and predictable ways. Programming DOS was a shit-show, of course, but so were non-trivial compilers. Nothing was ready.
Now we know how to do program better, have the power to run the compilers, and the legacy machines have a cost model I like to think of as "molasses in capillaries with huge bottlenecks". We're ready.
[1]: https://en.wikipedia.org/wiki/Structural_rule https://en.wikipedia.org/wiki/Structural_rule
- fallat 7y agoAre the arrows presented in the paper, something you think I should really familiarize myself with and use? I did a deep dive into lambda calculus over the past year and I noticed similar limitations you mention. So this seems interesting. I have seen arrows before but they just seem like a re-hash of the other lambda-like calculi. But maybe this paper's version of arrows is different?
- Ericson2314 7y agoI think it's worth it. Everything is lambda-in-a-straight-jacket-like. The question is how can you mix and match straight jackets, and how convoluted is programming. Also look at https://github.com/conal/concat https://github.com/conal/concat
- zozbot234 7y agoCategorical logic reframes the lambda calculus as being "simply" the internal language of cartesian-closed categories. Doing the same for other categories leads to other languages that are not so lambda-like. Sometimes categories are best characterized by graphical languages, as seen in string diagrams and generalizations thereof. Studying these things involves a rather thriving subfield at the intersection of PLT, category theory and foundational mathematics/logic.