Hacker News new | ask | show | jobs
by evincarofautumn 2771 days ago
The language they introduce, Π, is essentially a simple concatenative programming language where all of the primitive combinators happen to be reversible; the graphical depiction is essentially the same as graphical linear algebra¹, which is no coincidence. Concatenative combinator calculus is related to combinatory logic—specifically, it’s a variation that replaces application of combinators with composition, leading to a bunch of nice mathematical properties. Both of these logics have the nice feature that you can syntactically restrict the substructural rules of contraction (dropping), exchange (swapping), and weakening (copying): for example, a well-formed program that doesn’t use the K combinator to drop a value is guaranteed to be linear, i.e., not destroy any information. This isn’t true in ordinary lambda calculus, where you can use a variable zero or many times, so you need additional checks on the uses of a variable to determine whether a function is linear, affine, &c.

I like the theory of concatenative programming languages because they provide an elegant compositional/dataflow-oriented style of programming, have deep connections to linear logic, Hughes’ “arrows”, effects & coeffects, and quantum/reversible computation, while also admitting very efficient implementation on classical hardware.

I’m (very slowly) working on a statically typed low-level concatenative language that’s meant to provide all the nice high-level typed functional language features like higher-order functions, pipeline-style programming, and effects tracked in the types, while requiring no runtime support such as a tracing garbage collector—the ultimate goal is to allow a restricted subset that doesn’t even require a heap allocator, so you could use it to implement e.g. a kernel or device firmware. I hope that concatenative languages find their way to the mainstream as the basis for programming quantum and extremely low-power computing devices (which we will need in order to reduce emissions).

¹ https://graphicallinearalgebra.net/