Options

Compiling to Categories

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:

https://github.com/jmgimeno/categories-working-hacker/blob/master/src/Compiling/Interpretation/Abstract.hs#L19

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:

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

  • 1.

    @Matthew,

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

    Comment Source:@Matthew, do we have to create a new class for categories with fixed points with a `fix`operation?
  • 2.

    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.

    Comment Source: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.
  • 3.

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

    Comment Source:@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.
  • 4.
    edited May 17

    @Matthew,

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

    Comment Source:@Matthew, me neither :-D But, for the moment, this CategoryFix will have to wait because it is way down in my work stack :-(
Sign In or Register to comment.