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

- All Categories 2.2K
- Applied Category Theory Course 347
- Applied Category Theory Seminar 2
- Exercises 149
- Discussion Groups 48
- How to Use MathJax 15
- Chat 475
- Azimuth Code Project 108
- News and Information 145
- Azimuth Blog 148
- Azimuth Forum 29
- Azimuth Project 190
- - Strategy 109
- - Conventions and Policies 21
- - Questions 43
- Azimuth Wiki 708
- - Latest Changes 700
- - - Action 14
- - - Biodiversity 8
- - - Books 2
- - - Carbon 9
- - - Computational methods 38
- - - Climate 53
- - - Earth science 23
- - - Ecology 43
- - - Energy 29
- - - Experiments 30
- - - Geoengineering 0
- - - Mathematical methods 69
- - - Meta 9
- - - Methodology 16
- - - Natural resources 7
- - - Oceans 4
- - - Organizations 34
- - - People 6
- - - Publishing 4
- - - Reports 3
- - - Software 20
- - - Statistical methods 2
- - - Sustainability 4
- - - Things to do 2
- - - Visualisation 1
- General 39

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 :-(`