It looks like you're new here. If you want to get involved, click one of these buttons!

- All Categories 2.3K
- Chat 499
- Study Groups 18
- Petri Nets 9
- Epidemiology 3
- Leaf Modeling 1
- Review Sections 9
- MIT 2020: Programming with Categories 51
- MIT 2020: Lectures 20
- MIT 2020: Exercises 25
- MIT 2019: Applied Category Theory 339
- MIT 2019: Lectures 79
- MIT 2019: Exercises 149
- MIT 2019: Chat 50
- UCR ACT Seminar 4
- General 67
- Azimuth Code Project 110
- Statistical methods 3
- Drafts 2
- Math Syntax Demos 15
- Wiki - Latest Changes 3
- Strategy 113
- Azimuth Project 1.1K
- - Spam 1
- News and Information 147
- Azimuth Blog 149
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 708

Options

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) -- ...

Unfortunately, `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:

- Barr,
*Fixed points in cartesian closed categories*(1990) - Simpson and Plotkin,
*Complete axioms for categorical fixed-point operators*(2000) - Mulry,
*Categorical fixed point semantics*(1990)

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.

## Comments

@Matthew,

do we have to create a new class for categories with fixed points with a

`fix`

operation?`@Matthew, do we have to create a new class for categories with fixed points with a `fix`operation?`

Speaking for the less-experienced, I found Elliott's 2017 talk on the same paper ( http://podcasts.ox.ac.uk/compiling-categories ) a very helpful start.

`Speaking for the less-experienced, I found Elliott's 2017 talk on the same paper ( http://podcasts.ox.ac.uk/compiling-categories ) a very helpful start.`

@Juan

I am so sorry for missing this!

I am not sure how to create

`CategoryFix`

... if you read Elliot's paper he leaves it up in the air.His subsequent paper on automatic differentiation does not use recursion or fixed points, for better or for worse.

`@Juan I am so sorry for missing this! I am not sure how to create `CategoryFix`... if you read Elliot's paper he leaves it up in the air. His subsequent paper on automatic differentiation does not use recursion or fixed points, for better or for worse.`

@Matthew,

me neither :-D But, for the moment, this CategoryFix will have to wait because it is way down in my work stack :-(

`@Matthew, me neither :-D But, for the moment, this CategoryFix will have to wait because it is way down in my work stack :-(`