Polymorphise the type of some functions#319
Conversation
utdemir
left a comment
There was a problem hiding this comment.
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.
src/Prelude/Linear/Internal.hs
Outdated
| curry f x y = f (x, y) | ||
|
|
||
| -- | Beware, 'uncurry' is not compatible with the standard one because it is | ||
| -- higher-order and we don't have multiplicity polymorphism yet. |
There was a problem hiding this comment.
Perhaps this comment needs an update now that the function uses multiplicity polymorphism.
There was a problem hiding this comment.
+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.
src/Prelude/Linear/Internal.hs
Outdated
| ($) :: (a %1-> b) %1-> a %1-> b | ||
| ($) :: (a %p-> b) %1-> a %p-> b | ||
| -- XXX: Temporary as `($)` should get its typing rule directly from the type | ||
| -- inference mechanism. |
There was a problem hiding this comment.
You can remove the comment per ghc-proposals/ghc-proposals#406
7f57079 to
01604c9
Compare
|
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 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 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. |
01604c9 to
6d39961
Compare
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](https://gitlab.haskell.org/ghc/ghc/-/merge_requests/4632) to 9.0 prior to release, and as he hinted to me last week, it does make this polymorphisation possible. Closes #309 .
6d39961 to
f3aff2f
Compare
|
Mmm… so I had to inline a couple of things in the Hashmap tests where there were definition like: let (#.) = (Linear..) inThe reason, I imagine, is that we are performing defaulting too eagerly in lets. It is not affected by |
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:
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 .