4 ms·

I'm sorry I've spent half an hour with [3] and it's pretty challenging. Is there something with training wheels?

• carapace 8y ago
  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 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: [4 5 ...] 3 2 1 . pop swap roll< rest rest cons cons [4 5 ...] 3 2 . swap roll< rest rest cons cons [4 5 ...] 2 3 . roll< rest rest cons cons 2 3 [4 5 ...] . rest rest cons cons 2 3 [5 ...] . rest cons cons 2 3 [...] . cons cons 2 [3 ...] . cons [2 3 ...] . 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: (--) ∘ pop swap roll< rest rest cons cons (a1 --) ∘ swap roll< rest rest cons cons (a3 a2 a1 -- a2 a3) ∘ roll< rest rest cons cons (a4 a3 a2 a1 -- a2 a3 a4) ∘ rest rest cons cons ([a4 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ rest cons cons ([a4 a5 ...1] a3 a2 a1 -- a2 a3 [...1]) ∘ cons cons ([a4 a5 ...1] a3 a2 a1 -- a2 [a3 ...1]) ∘ cons ([a4 a5 ...1] a3 a2 a1 -- [a2 a3 ...1]) ∘ 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-programmers-the-preface/ https://bartoszmilewski.com/2014/10/28/category-theory-for-p... [1] http://www.kevinalbrecht.com/code/joy-mirror/j02maf.html http://www.kevinalbrecht.com/code/joy-mirror/j02maf.html [2] http://www.kevinalbrecht.com/code/joy-mirror/j04alg.html http://www.kevinalbrecht.com/code/joy-mirror/j04alg.html