Turn Join into a class for neater type signatures#399
Conversation
bd8608c to
32f0c27
Compare
| Optic k % Optic l = Optic m | ||
| where | ||
| km :: forall p i. Profunctor p => Optic_ m p i (Curry is i) s t u v | ||
| km = joinKinds @k @l @m @p k |
There was a problem hiding this comment.
These joinKinds are essentially the same as castOptic? Should we have castOptic-like function which uses joinKinds?
Do we need Is at all, isn't Is k l JoinKinds k l l? I don't suggest we need to remove Is, I just wonder how JoinKinds is related.
There was a problem hiding this comment.
These joinKinds are essentially the same as castOptic?
Yes, it's basically an extended version of implies you can use for both k and l.
Should we have castOptic-like function which uses joinKinds?
Is is used for expressing a subtyping relation, while JoinKinds for composition. It's true that they look very similar, but have distinct use cases.
Do we need Is at all, isn't Is k l JoinKinds k l l?
Yes, it looks like it. Functionally it could be used in place of Is, but it would be weird to users. Plus error messages in overlappable instances are different.
There was a problem hiding this comment.
I agree that their use cases are different, and thus repeating is not bad (especially as it is codegen).
There was a problem hiding this comment.
Is there a reason to prefer this encoding over reusing Is like this?
class (Is k m, Is l m) => JoinKinds k l m | k l -> mThere was a problem hiding this comment.
JoinKinds won't be newtype anymore. It might affect optimizer. If it doesn't, I'd like this sanity check.
There was a problem hiding this comment.
Is there a reason to prefer this encoding over reusing
Islike this?class (Is k m, Is l m) => JoinKinds k l m | k l -> m
We'd need to enumerate all cases anyway and we use the same codegen for it as for the Is instances.
I also don't know if there can be any complications like errors from Is being printed when overlappable error instance for JoinKinds is picked.
There was a problem hiding this comment.
Fair points. I'm happy with the plan here, feel free to merge.
I can imagine one might know JoinKinds and yet need Is, but only if one is doing something pretty close to optics internals, so let's worry about that if we ever find such a case.
In another context (HasField-related) I find myself wishing that one could define magically-contracted constraint synonyms, e.g. define
type Is k l = JoinKinds k l land have GHC print Is instead of JoinKinds in inferred types and error messages whenever they are equivalent. Perhaps one day...
|
BTW I noticed that type signatures before were quadratic in terms of length of the pipeline, since e.g. in a signature for The typeclass makes them linear. |
adamgundry
left a comment
There was a problem hiding this comment.
This generally looks good to me. I guess we are losing a small amount of expressiveness by dropping the type family, e.g. you needed to (re)introduce ReadOnlyOptic, but I'm inclined to think the more explicit approach is better. The type inference improvements are very welcome!
| Optic k % Optic l = Optic m | ||
| where | ||
| km :: forall p i. Profunctor p => Optic_ m p i (Curry is i) s t u v | ||
| km = joinKinds @k @l @m @p k |
There was a problem hiding this comment.
Is there a reason to prefer this encoding over reusing Is like this?
class (Is k m, Is l m) => JoinKinds k l m | k l -> m|
I'll merge after the weekend if there are no objections. |
Somewhat related to https://gitlab.haskell.org/ghc/ghc/-/issues/19336 (it's a GHC bug, but it pushed me to find a solution for using a class for
Jointhat works).I wanted to do that for some time now, considering that the type signature of
%was a bit messy, not to mention type signatures of generic optic functions (see e.g. #368). Now looks like a good time to do that sinceAppendwas also changed.Now the signature of
%is quite neat:Also, now label compositions are somewhat readable:
instead of this monstrosity
See also change to
label6setterin code, no more weirdIsconstraints.If no one protests, I'll adjust codegen.