Add support for kinds with type restrictions (#203)

[Kalin-Rudnicki]

No description provided.

[joroKr21]

If we're doing this we should add a lower bound too. And I wouldn't call this TypeRestriction but LB and UB or Lower and Upper, something like that.

[Kalin-Rudnicki]

I can make that change!

[milessabin]

Now that #206 has been merged I think this belongs in a separate library, or at least a separate module.

In particular I think that adding bounds to the existing Knn in this way complicates the typical cases in a significant way (I think the impact on type inference will likely be negative) to support a generalisation which could be easily handled via a separate set of kind definitions.

[Kalin-Rudnicki]

@milessabin since 206 was merged, my motivation to need to merge the change I was suggesting is much less. That being said, I think those are probably the 2 most common kinds with bounds, and might benefit a library user at some point. I am curious why you think type inference would be affected? In this case K1 and K11 are exactly as they are before, they are just extending from K1T/K11T, and locking in the bounds.

[milessabin]

In this case K1 and K11 are exactly as they are before, they are just extending from K1T/K11T, and locking in the bounds.

Possibly I'm being over cautious here. It would be good to test the new definitions against kittens at least.

Aside from that I think the irregularity bothers me. Why no similar treatment for K2? Why is the bound on K11,

Kind[C, O[_[_ <: TypeRestriction]]]

rather than,

Kind[C, O[_[t] <: TypeRestriction[t]]]

for instance?

In the absence of true kind polymorphism we have to stop somewhere. The current set of kinds is adequate for all of cats (@joroKr21 is that true? I think it is), which makes it a fairly salient place to rest.

[joroKr21]

I think the impact on type inference will likely be negative

I doubt that.

It would be good to test the new definitions against kittens at least.

Agreed, that would be a good smoke test.

Aside from that I think the irregularity bothers me. Why no similar treatment for K2?

Me too - if we add support for bounds, it should be on all current kinds.

Why is the bound on K11,

Actually I think it should be:

Kind[C, O[_] >: LB <: UB]

So that LB and UB can be either type lambdas or whatever is needed

The current set of kinds is adequate for all of cats (@joroKr21 is that true? I think it is), which makes it a fairly salient place to rest.

Yes, that's true.

I wonder if it's possible somehow to make use of AnyKind but it doesn't seem possible

[milessabin]

Actually I think it should be:

Kind[C, O[_] >: LB <: UB]

So that LB and UB can be either type lambdas or whatever is needed

Agreed that both upper and lower bounds would be needed for symmetry, however that's missing the point I was making, which was that a bound on a type of kind * -> * could be another type of kind * -> * rather than a type of kind *.

There is literally no end to this, which I why I chose to draw the line where I did.

@joroKr21 you're the primary maintainer now, so this is your call, but I think you'll be making your life difficult if you go down this road.

[joroKr21]

Agreed that both upper and lower bounds would be needed for symmetry, however that's missing the point I was making, which was that a bound on a type of kind * -> * could be another type of kind * -> * rather than a type of kind *.

I think it might work with type lambdas in Scala 3 but if I'm wrong about that then I agree it's not worth the hassle. We have to try first

[milessabin]

I think it might work with type lambdas in Scala 3

I think the type variable is essential ... T[t] <: U[t] isn't the same bound as T[_] <: U[_] because the second _ is interpreted as implicitly quantified, ie. more or less equivalent to T[_] <: U[Any] where U is covariant.

Which raises another issue ... what about variance? Each variance annotation creates a new kind.

[joroKr21]

Ah yeah it doesn't work as I expected:

scala> class Foo[F[_] <: [x] =>> List[x]]
// defined class Foo

scala> new Foo[List]
-- Error: ----------------------------------------------------------------------
1 |new Foo[List]
  |        ^^^^
  | Type argument List does not have the same kind as its bound [_$1] <: List
1 error found

scala> class Foo[F <: [x] =>> List[x]]
// defined class Foo

scala> new Foo[List]
val res0: Foo[List] = Foo@50df37eb