con-kitty / categorifier

Interpret Haskell programs into any cartesian closed category.
BSD 3-Clause "New" or "Revised" License
57 stars 2 forks source link

Categorifier imposes a `ClosedCat` constraint where not theoretically necessary #88

Open agrue opened 1 year ago

agrue commented 1 year ago

Hi there. I've been trying to use Conal's original plugin for automatic differentiation and was excited to find you had created this alternative! I've had no luck using it for AD so far though... when I try to categorify my expression into Conal's RAD category I get the error:

...
  - couldn't build dictionary for constraint

ClosedCat (GD (Dual (-+>)))

required by curry @ (GD (Dual (-+>))).
...

The same expression works fine with Conal's plugin. I have a very shaky understanding of these plugins, but as I understand it Conal's plugin does considerable work to avoid imposing the ClosedCat constraint (i.e. generating a curry or uncurry) because many of the categories he's working with aren't actually Cartesian closed (like RAD aka GD (Dual (-+>))). So I'm wondering if you decided to forget about all that complexity in favor of just requiring that the destination category be Cartesian closed. If so I suppose I'll just go back to Conal's plugin (with some regret - I love the quality of your error messages!)

If you think this is a bug and automatic differentiation should actually work then I'll provide more detail, I just thought I should ask the philosophical question first. Thanks!