Re:Lost in Math
by carapace on Sunday July 01, 2018 @08:46PM
(#17438605)
I don't know. It's kind of newfangled. It's "in the air" though, I think. Here's what I got (it helps to know a little Category Theory, try Bartosz Milewski's "Category Theory for Programmers"[0] if you don't already.)
In "Compiling to Categories" what he’s doing is translating lambda forms into a kind of “point-free” style and then showing how to instantiate that code over different categories to get several different kinds of program out of the same code.
I've been working with a stack-based "concatinative" language called Joy which I think makes this stuff a lot clearer. Joy code is already in "point-free" style (no vars, no lambdas) and it includes functions that do the same job as but are more elegant than the triangle operators and others in the "squiggol" tradition. ( https://wiki.haskell.org/Pointfree )
There's a little bit in "Mathematical foundations of Joy"[1] and "The Algebra of Joy"[2] by Manfred von Thun.
Here's a piece of Joy code (it's part of an ordered binary tree library):
pop swap roll< rest rest cons cons
Here's a trace of its evaluation (with a suitable value already on the stack) in the category of values resulting in a computation of an answer. The dot is the "interpreter head", the current point of evaluation:
If you compare the input and output of the first one you'll see that it matches the input and output stacks in the Forth-style stack effect comment computed by the second one.
To repeat, that's the same code evaluated in two different domains, er, Categories, to get two different correct computations.
If I had implementations for them I could evaluate the expression in/over a category and get as output: a dataflow diagram of the program, or a hardware description of a circuit for the program, which are examples from Elliott's talk+paper.
In "Compiling to Categories" what he’s doing is translating lambda forms into a kind of “point-free” style and then showing how to instantiate that code over different categories to get several different kinds of program out of the same code.
I've been working with a stack-based "concatinative" language called Joy which I think makes this stuff a lot clearer. Joy code is already in "point-free" style (no vars, no lambdas) and it includes functions that do the same job as but are more elegant than the triangle operators and others in the "squiggol" tradition. ( https://wiki.haskell.org/Pointfree )
There's a little bit in "Mathematical foundations of Joy"[1] and "The Algebra of Joy"[2] by Manfred von Thun.
Here's a piece of Joy code (it's part of an ordered binary tree library):
Here's a trace of its evaluation (with a suitable value already on the stack) in the category of values resulting in a computation of an answer. The dot is the "interpreter head", the current point of evaluation: And here's the same code evaluated in a category of composition of stack effects resulting in a description of the stack effect of the expression: If you compare the input and output of the first one you'll see that it matches the input and output stacks in the Forth-style stack effect comment computed by the second one.To repeat, that's the same code evaluated in two different domains, er, Categories, to get two different correct computations.
If I had implementations for them I could evaluate the expression in/over a category and get as output: a dataflow diagram of the program, or a hardware description of a circuit for the program, which are examples from Elliott's talk+paper.
[0] https://bartoszmilewski.com/2014/10/28/category-theory-for-p...
[1] http://www.kevinalbrecht.com/code/joy-mirror/j02maf.html
[2] http://www.kevinalbrecht.com/code/joy-mirror/j04alg.html