Open cartazio opened 6 years ago
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?
It's just something I've not gotten around to. I think it requires roughly the following:
let
bindings but not global bindings, so some analysis is necessary.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.
Great! I haven’t worked on it at all. I’m happy to help with design issues and implementation if you like.
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.
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 freshVar
) and wrap it inData.Function.fix
. Thenfix
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)
becomesfixC @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 = ()
).
fixC @(->) @()
is isomorphic to base's fix
.
I guess
a = ()
andx = a -> b
, sofixC
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.
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
Thanks. I see my mistake now.
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.
we chatted about how thats current a no go at ICFP 2017, has there been any action on that since?