Really interesting. As well he seems to re-derive and implementation of Forth.
In episode 6, Right under the diagran for Crema di Marscapone he has a formula.
Does anyone that uses Forth know if it has that circle-plus operator? It seems to really lend to conciseness - and I hadn't remembered anything like it last time I looked at Forth.
It’s not surprising—there’s a deep relationship among concatenative languages, Hughes’ arrows, combinator calculus, category theory, linear algebra, logic, even topology. I haven’t read through this but I guess the ⊕ operator would be “* * *” (parallel composition) in arrow notation; in Haskell it has the type “Arrow a ⇒ a b c → a b′ c′ → a (b, b′) (c, c′)”, or “(b → c) → (b′ → c′) → (b, b′) → (c, c′)” specialised to the function arrow.
I've been looking for a categorical take on neural networks and have found nothing, and this might get me started into translating some existing NN papers to CT.
I think the major difference is this notation has the count of loose wires corresponding to dimension, and Penrose notation has the count of loose wires corresponding to tensor valence.
Here, a diagram with 1L and 2R wires corresponds to a 2d-vector, in Penrose's notation it would correspond to a (1,2) tensor that takes kd-vectors to kXk matrices.
But... they certainly have a similar feel. I wonder if you could build up the Penrose notation out of this.
The structure is more obviously modular and the algebraic laws become topological phenomena, which makes it easier to consider more complicated structures than vector spaces.
