Add support for linear types. #70
Conversation
sellout
force-pushed
the
linear
branch
3 times, most recently
from
443043f
to
2645778
Compare
sellout
force-pushed
the
linear
branch
6 times, most recently
from
61a5d57
to
45769a7
Compare
sellout
force-pushed
the
linear
branch
6 times, most recently
from
077dea4
to
98c35c1
Compare
|
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. |
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. |
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.
Unfortunately, I don't think there's a reasonable way to conditionalize the linear-base-integration packages until Cabal 3.8 is released. Once nix-flake integration (#66) is merged, we can perhaps do it for _those_ builds.
| [Plugins.Type _mult, Plugins.Type _cat, Plugins.Type _a] -> pure Nothing | ||
| [Plugins.Type _mult, Plugins.Type _cat] -> pure Nothing | ||
| [Plugins.Type _mult] -> pure Nothing | ||
| [] -> pure Nothing |
There was a problem hiding this comment.
From this to line 544, it's the same as non-linear version. we had better minimize conditional compilation part.
There was a problem hiding this comment.
This can be difficult with Ormolu. They've changed the way CPP is handled a few times, but I think the current approach is that CPP directives are treated as comments, and then the module is formatted.
Generally, this means that putting directives around top-level definitions works just fine. Other cases may work, but are more fragile. Here, shrinking the directives to only cover some of the case alternatives causes a parse error. I'm not sure exactly why, as it seems like treating the directives as comments should allow that to work. But I'm guessing there's some subtlety in the CPP handling that I'm missing.
There was a problem hiding this comment.
I see. yeah. I was often bitten by ormolu and CPP incompatibility. If not easily fixable, please disregard my suggestion.
|
It's neat that no change needs to be made to |
No changes yet. Making the linear interpretation simpler than the standard one will certainly involve changes there. |
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.