what is the current status of support for recursive definitions?

[cartazio]

we chatted about how thats current a no go at ICFP 2017, has there been any action on that since?

[agrue]

I'm curious about this too. Specifically I'm interested in deriving backpropagation for RNNs, e.g. LSTM. When I try the straightforward approach of folding over the inputs the CCC translation seems to get hung up on the recursive let binding.

What makes this a "no go" currently?

[conal]

It's just something I've not gotten around to. I think it requires roughly the following:

• Choose an algebraic/categorical interface to which to translate recursion (say a trace).
• Translate recursive GHC Core definitions into the chosen interface.
  This step seems delicate, e.g.,
  • Haskell handles recursive definitions for non-functions, which I don't know how to translate.
  • GHC Core explicitly flags recursive local let bindings but not global bindings, so some analysis is necessary.
  • Mutually recursive definitions need to be combined into one and separated out at their uses.
• Implement instances of the chosen interface for various categories.
  For automatic differentiation in particular, look for supporting properties of differentiation as in theorems 1–3 of The simple essence of automatic differentiation.

[sellout]

I think I'm going to try tackling part of this. I only need to support non-mutually-recursive local let bindings (I'm pretty sure). Curious whether the past year has given you any more thoughts on how to approach this.

Thanks.

[conal]

Great! I haven’t worked on it at all. I’m happy to help with design issues and implementation if you like.

[sellout]

The approach I've implemented is to "unfix" any recursive definition (subst the recursive references with a fresh Var) and wrap it in Data.Function.fix. Then fix gets converted to the traced Cartesian notion of fix:

fixC :: Prod k a x `k` x -> a `k` x

so, fix @(a -> b) becomes fixC @cat @() @(a ->b) (the extra parameter is always @()). I think this satisfies my case, and I think can use the same approach for non-mutually-recursive global definitions (we've moved inlining internal to the plugin, so after looking up the unfolding, I can check whether the identifier we're inlining is free in the unfolding for that same identifier).

I'd like to be able to weaken the conversion so I can get away with traced monoidal, instead of traced Cartesian in some cases, but I'm not sure how to do that.

[conal]

How wonderful to hear of activity on this front!

The approach I’ve implemented is to “unfix” any recursive definition (subst the recursive references with a fresh Var) and wrap it in Data.Function.fix. Then fix gets converted to the traced Cartesian notion of fix:

fixC :: Prod k a x `k` x -> a `k` x

That fixC type surprises me. I expected ((a × z) `k` (b × z)) -> (a `k` b) as in a traced monoidal category. Or something akin to (a -> a) -> a as in Haskell.

How did you come up with your type?

so, fix @(a -> b) becomes fixC @cat @() @(a ->b) (the extra parameter is always @()).

Which is the “extra parameter” here? By argument order, I guess a = () and x = a -> b, so fixC essentially has type (a `k` b) -> (a `k` b), which seems unlikely (though likelier than x = ()).

[sellout]

fixC @(->) @() is isomorphic to base's fix.

I guess a = () and x = a -> b, so fixC essentially has type (a `k` b) -> (a `k` b),

The first half of this is correct, but this means fixC @(->) has type (((), a -> b) -> a -> b) -> () -> a -> b, so removing the units ends up as ((a -> b) -> a -> b) -> a -> b (i.e., the same as Data.Function.fix) -- and this should work even if the recursive binding isn't a function (say in the case of building a record lazily where some fields depend on the values of others), where we get (a -> a) -> a, truly as general as Data.Function.fix.

This fixC is from section 3.1 of http://www.kurims.kyoto-u.ac.jp/~hassei/papers/tlca97.pdf, and I believe the extra parameter is necessary for a categorical version of a fixed point (although since the category must be Cartesian to have fixC that extra parameter could be restricted to the Unit, I suppose, which is what I'm doing when translating fix from base).

To summarize that paper (and a couple other sources, where I don't remember what comes from which):

A traced monoidal category has a trace like ((a × z) `k` (b × z)) -> (a `k` b), if that category is also Cartesian monoidal, you get a morphism like fixC. trace and fixC are each definable in terms of the other in that case.

So, I was able to come up with a translation in terms of fixC (which is pretty trivial since fix is right there for us), but that requires that the target category is Cartesian. So yeah, a translation that used trace instead of fixC (in at least some cases) would be preferable, but I'm not sure how to take that step.

[sellout]

Oh, yeah, the nLab page you linked has a brief section on the "parameterized fixed-point" and a reference to the paper I linked: https://ncatlab.org/nlab/show/traced+monoidal+category#in_cartesian_monoidal_categories

[conal]

Thanks. I see my mistake now.

[sellout]

A small update to this. I had said "the extra parameter is always ()", but it's not.

Here's a short conversion:

fix :: (a -> a) -> a
fixC :: (x, a) `k` a -> x `k` a

-- the starting point of the conversion, thus the goal is @x `k` a@
(\x -> fix U) :: x -> a

goLam x U :: x `k` a -> a
uncurry (goLam x U) :: (x, a) `k` a
fixC (uncurry (goLam x U)) :: x `k` a

So, the extra parameter is the Var of the Lam we're converting. This is quite a nice mapping.