Polymorphise the type of some functions

[aspiwack]

What I've done is take the prelude functions that we use all the time
and polymorphise the higher-order arrows.

I left the first order arrow to multiplicity 1 whenever possible
because:

• We can cast them to any multiplicity by a simple 𝜂-expansion
• Any multiplicity involving multiplicity multiplication will hit the
  limitations of the type checker currently (it doesn't know that
  multiplication is associative, typically), so I really wanted a
  single multiplicity variable per type.

This does leave composition fully linear, unfortunately, because there
are two (independent) higher-order arrow, and there is no most general
choice of one to polymorphise.

It didn't work last time I tried, but @monoidal made a cleverly short
patch to
9.0 prior to release, and as he hinted to me last week, it does make
this polymorphisation possible.

Closes #309 .

[utdemir]

This is great! I also remember making them polymorphic was making type-checker confused, so it's nice that this got solved. The fact that the rest of the linear-base still compiles without any more annotations convince me that this is a good idea.

[facundominguez]

Perhaps this comment needs an update now that the function uses multiplicity polymorphism.

[monoidal]

+1. You can generalize the remaining linear argument for curry and then remove the comment, it will completely subsume the one in Prelude. I've tried

($) :: (a %p-> b) %q-> a %p-> b
(&) :: a %p-> (a %p-> b) %q-> b
const :: a %m-> b -> a
asTypeOf :: a %m-> a -> a
($!) :: (a %p-> b) %q-> a %p-> b
curry :: ((a, b) %p-> c) %q-> a %p-> b %p-> c
uncurry :: (a %p-> b %p-> c) %q-> (a, b) %p-> c
forget :: (a %1-> b) %m-> a -> b

and the testsuite passed. I think it's reasonable to expect this to work at this complexity in 9.0. If there is a place where the monomorphic version works but the polymorphic doesn't, please let me know.

[monoidal]

You can remove the comment per ghc-proposals/ghc-proposals#406

[aspiwack]

I (finally!) came back and addressed the comments.

The reason why it's taken me that long is because I was hesitant to make all the first-order arrows multiplicity-polymorphic as @monoidal suggested.

Here's the thing: the fact that I can do that is due to the fact that we have a built-in rule in the compiler that every multiplicity is compatible with exactly-once consumption. This precludes some possible further multiplicities (like the dreaded 0, or a multiplicity saying “exactly twice”. While I don't really think that we will ever need a multiplicity “exactly twice”, I consider it healthy to make a compatible system).

So why do we have this rule? Well, we absolutely positively needed it for backward compatibility of the constructors (constructors are linear by default, but they are currently used as unrestricted functions in many places): constructors expose a polymorphic interface. Since we don't have a way, yet, to express a “p is compatible with exactly-once consumption” constraint (which I imagine will be spelt something like 'One <= p), we simply internalised it.

I was very hesitant to extend the use of this, which I consider to be a hack in the system beyond this internal use. On the other hand, we have a similar problem with this prelude functions as with the constructors, if we want the function to be a drop-in replacement. And so I agonised for weeks (and had several discussions with @monoidal off band).

He finally convinced me that it was the way to go and to embrace the hack. Basically, because we need the 'One <= p rule for the sake of compatibility, the only way we can add incompatible multiplicity is by adding such a constraint first. When that happens we can upgrade all our functions to use it.

I wouldn't advertise that people necessarily use this style except when backward compatibility like this is a prime concern, as it is code that may break whenever we figure out our story here. But for linear-base, it's almost certainly the way to go.

[aspiwack]

Mmm… so I had to inline a couple of things in the Hashmap tests where there were definition like:

let (#.) = (Linear..) in

The reason, I imagine, is that we are performing defaulting too eagerly in lets. It is not affected by -XMonoLocalBinds. I think that it's fine for now. I could have added a type signature to (#.) as well, but that felt unnecessary.