GitLab

Summary

I'm just starting to try to understand linear types, from the users guide: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html

I've made my best effort to read the entry closely a couple times, as well as experiment a little, and have some questions. I don't understand things well enough to offer a PR that improves things, unfortunately; hopefully hearing what's confusing to a newbie is constructive.

I don't understand what "use" or "consume" means.

The bulleted definition doesn't seem sufficient. aspiwack-tweag on reddit suggests "use" has something to do with evaluation, and so I wonder if a base case should be added to that bullet list. I'm looking for something precise, like the docs for seq.

"multiplicity polymorphism" feels pretty slippery

The docs begin...

A function f is linear if: when its result is consumed exactly once, then its argument is consumed exactly once.

So I expect that...

id a = a

...is by that definition linear.

Yet we can give it the type signature id :: a %m -> a, which my intuition says ought to be a rigid type error. Maybe multiplicity is just a little... weird? It would help to call that out in the docs if so, even if a more satisfying answer is too much for the users guide.

Related: it seems only a function that "is linear" can be declared multiplicity-polymorphic. If that's so, I think adding this observation to the docs would help people like me.

The datatypes section starts talking about "linear fields" without defining them

It seems like "linear field" means a field that doesn't have to be "consumed exactly once" if it's on the LHS of a linear arrow. If that's so maybe an explanation to that effect to lead off the data types section, and a caveat mention in the "Pattern-matching" bullet point

In general I find it confusing to be using "unrestricted" or "linear" to refer to both values and arrows, but maybe that's pedantic.

Environment

• ghc 9.1.20201218 (what I have on hand...)