It looks like you're new here. If you want to get involved, click one of these buttons!
I wanted to start a splinter group from the Categories For the Working Hacker
Here, I wanted to talk about Conal Elliot's Compiling to Categories (2017) paper.
Juan Manuel Gimeno has been kind enough to post his code exploring this paper here.
Having worked through most of this paper, I wanted to point out an observation.
Here in Juan's code we have an attempt to interpret a term in a Turing-complete typed \(\lambda\)-calculus in categories like Conal's:
instance ( Closed k , ConstCat k , NumCat k Int , OrdCat k Int , BoolCat k ) => Language k where here = exl before f = f . exr lambda f = curry (f . swap) apply f g = applyC . (f |*| g) loop f = applyC . ( f |*| loop f) -- ...
loop takes advance of Haskell's laziness. Unfortunately
loop cannot be defined for any cartesian closed category. You need the category to have a fixed points. There is a an old theorem by Lawvere (1969) the gives sufficient conditions for this. Conal Elliot also notes on page 27 of his paper that the work in the following papers might help:
In general, Cartesian Closed Categories model the simply typed \(\lambda\)-calculus, which is strongly normalizing and not Turing complete.
This isn't a bad thing. Gabriel Gonzalez' Dhall configuration language is strongly normalizing, too.
I am quite interested in Elliot's work in compiling to vector spaces. I want to focus on understanding this.
I am hoping to find some overlap quantum physics. I know a lot of people are interested in that. It would be great if we could have a shared discussion.