should Kleisli contravariant on A?

[jcouyang]

Kleisli[F[_], A, B] is supposed to be abstraction of A => F[B], but => has type of Function1[-A, +B], I can't figure out why Kleisli is invariant on both A and B, is there any benefit that it's design like this?

from what I observed, it will be much easier to let scala compiler find out what A should be

for instance, if I would like to choose from two Kleisli

contravariant on -A

case class Kleisli[F[_], -A, B](run: A => F[B])

def first[A, B, C, F[_]](a: Kleisli[F, A, B], b: Kleisli[F, A, C]) = a

trait A1
trait A2
trait A12 extends A1 with A2

first(Kleisli((a: A1) => Some(a)), Kleisli((b:A2)=>Some(b)))
res7: Kleisli[Some, A2 with A1, A1] =  ...

compiler can infer the correct type of the input of Kleisli should be A2 with A1 and the output will be A1

to achieve the same thing without -A will be much difficult

by contramap

def first[A1, A2, A12, B, C, F[_]](a: Kleisli[F, A1, B], b: Kleisli[F, A2, C])
  (implicit ev: A12<:<A1):Kleisli[F, A12, B] = 
  Contravariant[Kleisli[F, ?,B]].contramap(a)(ev)

@ first(Kleisli((a: A1) => Some(a)), Kleisli((b:A2)=>Some(b)))
cmd14.sc:1: type mismatch;
 found   : Nothing <:< Nothing
 required: A12 <:< ammonite.$sess.cmd9.A1
val res14 = first(Kleisli((a: A1) => Some(a)), Kleisli((b:A2)=>Some(b)))
                 ^

the compiler can't infer A12 for contramap unless I explicitly tell the compiler that I need Kleisli[Some, A12, A1]

@ first(Kleisli((a: A1) => Some(a)), Kleisli((b:A2)=>Some(b))) : Kleisli[Some, A12, A1]
res14: Kleisli[Some, A12, A1] = Kleisli(scala.Function1$$Lambda$35/695682681@1e3c4c12)

[Maatary]

Hi @jcouyang I wonder if you could help me with some pointers on the issue you raised.

Although I understand the explanation above, and experienced it when composing Kleisli, I am looking for the formal definition of things.

What is the machanism that enable to compiler to infer A2 with A1, is it LUB in the context of contravariance. It seems to me that A2 with A1 is the LUB of A1 and A2.

I wonder if i can find those rules somewhere in the specification so that thing does not sound magic to me and is predictable.

[jcouyang]

hi @Maatary I think it is the other way around, A1 is upper bound of A2 with A1 so A2 with A1 is Highest Lower Bound of A1 or A2, since A2 with A1 <: A1 also A2 with A1 <: A2. + means subtype can be in supertype's place by covariance, now A is -A so supertypeKleisli[F, A1, B] is safe to be in its subtype Kleisli[F, A2 with A1,B] place
it should be pretty easy for compiler to infer a subtype for both A1 and A2 must be A2 with A1

def flatMap[C, AA <: A1](f: B => Kleisli[F, AA, C])(implicit F: FlatMap[F]): Kleisli[F, AA, C]

by constrain AA<:A1 AA must be subtype of A1, if you pass in f as f: B => Kleisli[F, A2, C], since contravariant, super type can be in subtype's position, f's type can be variant to any of A2 subtype, so AA must be subtype of both A2 and A1