News for hackers. Stuff that matters.
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:

    [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-p...

[1] http://www.kevinalbrecht.com/code/joy-mirror/j02maf.html

[2] http://www.kevinalbrecht.com/code/joy-mirror/j04alg.html

There are no comments on this comment yet.