search

con-kitty / categorifier

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

Add support for linear types. #70

Closed sellout closed 2 years ago

sellout commented 2 years ago

This doesn't yet take advantage of the linear optimizations, but it does allow us to categorify linear functions.

It adds a linear-base integration, because nothing in base uses linear-types, so we need something to test it with.

wavewave commented 2 years ago

Would you add some expanded explanation on the meaning of "support for linear types"? :-) Having that description in this PR's description message (and commit message as it automatically adds) is fine for me. Thanks.

sellout commented 2 years ago

Would you add some expanded explanation on the meaning of "support for linear types"? :-)

Whoops, I actually meant to add this to the README. I'll still update the readme before merging, but tl;dr for now:

https://arxiv.org/abs/2103.06195v1 is the goal – targeting symmetric monoidal categories instead of cartesian closed categories (when possible). This change however is just the first step, which merely allows us to interpret linear functions as if they weren't linear. The follow-up to this will be to preserve that linearity through the plugin.

We've been talking about adding this for like a year, but now I actually have a category in a project that isn't cartesian closed, so I'm finally motivated.

zliu41 commented 2 years ago

It's neat that no change needs to be made to categorify!

sellout commented 2 years ago

It's neat that no change needs to be made to categorify!

No changes yet. Making the linear interpretation simpler than the standard one will certainly involve changes there.