a solution for combining covariant and contravariant functions

[Vlad Patryshev]

Specifically, for collections, but it does not matter much.

Roughly, List is a covariant functor, Container (supertrait of Set) is contravariant; and we can have a natural transformation (implemented as an implicit) from one to another, and can have typed contains().

https://docs.google.com/document/d/1sC42GKY7WvztXzgWPGDqFukZ0smZFmNnQksD_lJzm20/edit?usp=sharing

Comments welcome.

Thanks,
-Vlad

[Paul Phillips]

On Mon, Aug 5, 2013 at 9:00 PM, Vlad Patryshev <vpatr...@gmail.com> wrote:

Comments welcome.

It only works because of type inference implementation details. Yes, this doesn't compile:

  val xs = HeadWithTail(5, HeadWithTail(10, EmptyList))

  println(xs contains "abc")

...but only because the type inferencer infers Int during the implicit conversion, then obstinately refuses to reconsider the situation. If it were more ambitious, it would find this:

  println((xs: MyList[Any]) contains "abc")

which compiles fine. You don't want this inference detail to be the foundation of anything.

The problem is inherent in any attempt to graft contains onto a covariant collection. If contains is applicable to the covariant type, then no matter how you try to obscure it, the Foo[T] is a Foo[Any] and its contains takes an Any.

However...

I believe I've found a more robust way out, but it won't happen in the "real" collections. An unexpected bonus was the invariant List. It's really nice not seeing my list of 1000 Ints quietly turn into a list of AnyVals when the 1001th element is a Double. How could that be what I meant? Now it's a type error.

// APIs - pure interfaces - all covariant - none has a contains method.

trait Foreach[+A] {

  def isEmpty: Boolean

  def foreach(f: A => Unit): Unit

}

trait Iterable[+A] extends Foreach[A] {

  def iterator: Iterator[A]

}

trait Mapping[-A, +B] {

  def apply(x: A): B

}

trait Seq[+A] extends Iterable[A]

trait Set[+A] extends Iterable[A]

trait Map[K, +V] extends Set[K] with Mapping[K, V]

trait IntMapping[+B] extends Mapping[Int, B] {

  def apply(x: Int): B

}

trait Contains[A] {

  def contains(x: A): Boolean

}

object Seq {

  trait Linear[+A] extends Seq[A] {

    def head: A

    def tail: Linear[A]

  }

  trait Indexed[+A] extends Seq[A] with IntMapping[A] {

    def size: Int

  }

}

// Leaf nodes - all final, concrete, invariant - contains method introduced here.

// If you need covariance, weaken to Seq[+A] and all you lose is contains and

// any other last minute arrivals.

final class Range private (start: Int, end: Int, step: Int, val size: Int)

  extends Seq.Indexed[Int] with Contains[Int] { ... }

sealed abstract class List[A] extends Seq.Linear[A] with Contains[A] { ... }

final case object Nil extends List[Any] { ... }

final case class ::[A](head: A, tail: List[A]) extends List[A] { ... }

// etc etc 

[Vlad Patryshev]

Paul,

Your robust solution is a very good step in the right direction.

But regarding your examples,

val xs = HeadWithTail(5, HeadWithTail(10, EmptyList))

  println(xs contains "abc") // does not compile

println((xs: MyList[Any]) contains "abc")

I believe this is the right behavior. We map MyList[Int] to MyList[Any]; sure then we can call contains("abc") on this new domain. 

Thanks,
-Vlad

--
You received this message because you are subscribed to the Google Groups "scala-language" group.
To unsubscribe from this group and stop receiving emails from it, send an email to scala-languag...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[Paul Phillips]

On Sat, Aug 10, 2013 at 11:28 AM, Vlad Patryshev <vpatr...@gmail.com> wrote:

val xs = HeadWithTail(5, HeadWithTail(10, EmptyList))

  println(xs contains "abc") // does not compile

println((xs: MyList[Any]) contains "abc")

I believe this is the right behavior. We map MyList[Int] to MyList[Any]; sure then we can call contains("abc") on this new domain. 

You aren't mapping MyList[Int] to MyList[Any]. It is already a MyList[Any]. This is an essential property - the essential property - of covariance.

The ascription is simply reminding the type inferencer of what it already knows to be true. It is an implementation detail that it doesn't come up with it on its own.

You absolutely cannot rely on any behavior which depends on a MyList[Int] being understood as precisely that and not as a MyList[T] forSome { type T >: Int }.

[Vlad Patryshev]

>You aren't mapping MyList[Int] to MyList[Any]. It is already a MyList[Any]. This is an essential property - the essential property - of covariance.

From the p.o.v. of category theory that's exactly what is happening, that's why I used the term 'map'.

Thanks,
-Vlad

[Sassa Nf]

I don't think that will be right, will it.

Using MyList[Int] where MyList[Any] is expected is one thing (mapping type A to B according to covariance), and telling the compiler to expect MyList[Any] where MyList[Int] is specified, is completely different (extend a arrow A->C to arrow B->C).

Suppose MyList is mutable. Casting MyList[Int] to MyList[Any] is obviously dangerous, and it shouldn't be a implementation detail that it doesn't assume that.


Alex

[Paul Phillips]

On Mon, Aug 12, 2013 at 8:55 AM, Sassa Nf <sass...@gmail.com> wrote:

Suppose MyList is mutable. Casting MyList[Int] to MyList[Any] is obviously dangerous, and it shouldn't be a implementation detail that it doesn't assume that.

If it's mutable it isn't covariant. This is another essential property of covariance.

[Paul Phillips]

On Sat, Aug 10, 2013 at 10:46 PM, Vlad Patryshev <vpatr...@gmail.com> wrote:

From the p.o.v. of category theory that's exactly what is happening, that's why I used the term 'map'.

I enjoy category theory as much as the next guy, but the list is "scala-language", not "category-theory-language", and category theory doesn't have a monopoly on the extremely generic term 'map'.

[Sassa Nf]

oh well... I missed that.

Yet all implicit conversions must occur only if the result is "the same" with or without the conversion. The "sameness" of result can be described as a natural transformation. For example, that's why it is "safe" to work out the sum of integers a+b as either Integer.+ or Float.+.

Here we have two natural transformations: covariance MyList[Int]->MyList[Any], and implicit toContainer MyList[Int]->Container[Int]. We also have contravariance Container[Any]->Container[Int].

In a way, Vlad's example permits exactly that - follow any path depending on implementation, because his Container is contravariant. But will it be allowed to follow any path to construct a Container that is not contravariant, like in your solution?


Alex

2013/8/12 Paul Phillips <pa...@improving.org>

On Mon, Aug 12, 2013 at 8:55 AM, Sassa Nf <sass...@gmail.com> wrote:

Suppose MyList is mutable. Casting MyList[Int] to MyList[Any] is obviously dangerous, and it shouldn't be a implementation detail that it doesn't assume that.

If it's mutable it isn't covariant. This is another essential property of covariance.

--
You received this message because you are subscribed to a topic in the Google Groups "scala-language" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/scala-language/eU0yPJq589Y/unsubscribe.
To unsubscribe from this group and all its topics, send an email to scala-languag...@googlegroups.com.

[Vlad Patryshev]

I understand the difference between category theory and Scala, but regarding the monopoly I have a different opinion; the closer we are to the right theory, the less problems (of conceptual kind) we will have in our practice.

Thanks,
-Vlad

[Paul Phillips]

On Mon, Aug 12, 2013 at 11:07 AM, Sassa Nf <sass...@gmail.com> wrote:

Here we have two natural transformations: covariance MyList[Int]->MyList[Any], and implicit toContainer MyList[Int]->Container[Int]. We also have contravariance Container[Any]->Container[Int].

No, the key transformations (speaking broadly, see below) are:

MyList[Int] -> Container[Int]

MyList[Any] -> Container[Any]

MyList[Int] -> MyList[Any]

The first two are instantiations of polymorphic MyList[T] -> Container[T], the last a formulation of covariance.

So given an expression

(xs: MyList[Int]) contains (x: Any)

Vlad's approach to making this a type error depends (possibly ironically) on the second and third not being composed, so that only the first can be applied. It is an implementation detail that they are not.

And although you may view it that way in category theory, scala doesn't consider MyList[Int] -> MyList[Any] to be a conversion. A MyList[Int] "is a" MyList[Any]. It hasn't spent any "conversion budget" on this, because it was already true exactly as it was. You have to throw out subtyping if you want to avoid this.

[Paul Phillips]

On Mon, Aug 12, 2013 at 11:52 AM, Vlad Patryshev <vpatr...@gmail.com> wrote:

I understand the difference between category theory and Scala, but regarding the monopoly I have a different opinion; the closer we are to the right theory, the less problems (of conceptual kind) we will have in our practice.

I have no problem with trying to use words in a precise way, but people still have to know what you mean if the point of the exercise includes the transmission of information. There's no prize awarded for being accurate according to one's own model if you aren't understood by the people down at sea level.

[Vlad Patryshev]

I know, I know. Just cannot stand terms like "ATM machine". Or when any function that takes a function and returns a function being called a functor. Just hoping that sea level is rising with time.

Thanks,
-Vlad

--

[Sassa Nf]

Yes, that's clear to me. What I am wondering about, is whether you can make the same decisions if there is no contravariance of Containers.

In other words, clearly, in the solution where we have all four structure-preserving maps:

MyList[Int]->Container[Int],

MyList[Int]->MyList[Any],

MyList[Any]->Container[Any],

Container[Any]->Container[Int]

we can permit the compiler to compose any of them, because they are completely identical representations of intent.

However, if we don't have contravariance Container[Any]->Container[Int], can we still permit the compiler to choose _any_ composition of arrows? They clearly do not represent the same intent anymore.


Alex

2013/8/12 Paul Phillips <pa...@improving.org>

[Paul Phillips]

On Tue, Aug 13, 2013 at 3:53 AM, Sassa Nf <sass...@gmail.com> wrote:

However, if we don't have contravariance Container[Any]->Container[Int], can we still permit the compiler to choose _any_ composition of arrows? They clearly do not represent the same intent anymore.

I don't think I understand the question, but I think we still can (must) permit the compiler to choose any composition of arrows. And there's nothing for which we need Container[Any]->Container[Int]  to arrive there.

I thought we were talking about soundness; if so, intent is irrelevant anyway. If I define x only as "x >= 0" and then define y as "x * -1", it might be my intent that y == 0 but that's not always how it's going to work out. The analogy is direct: a variant type parameter describes a range of types, and any derived type which exposes it must behave correctly over the whole range.

[Sassa Nf]

Of course, we can permit that. But how do you define "ambiguity requiring human intervention"?

In the case where we have contravariance Container[Any]->Container[Int] the ambiguity doesn't require human intervention, because either choice behaves in the same way. In the case where we don't have that contravariance, how to get a guarantee that both have the same algebraic structure; if we don't have this guarantee, we are letting the compiler quietly make a choice that we possibly didn't want.

Alex

2013/8/13 Paul Phillips <pa...@improving.org>

--

[Shelby]

On Tuesday, August 6, 2013 12:31:02 PM UTC+8, Paul Phillips wrote:

On Mon, Aug 5, 2013 at 9:00 PM, Vlad Patryshev <vpatr...@gmail.com> wrote:

Comments welcome.

It only works because of type inference implementation details. Yes, this doesn't compile:

  val xs = HeadWithTail(5, HeadWithTail(10, EmptyList))

  println(xs contains "abc")

...but only because the type inferencer infers Int during the implicit conversion, then obstinately refuses to reconsider the situation. If it were more ambitious, it would find this:

  println((xs: MyList[Any]) contains "abc")

I disagree. The contains method is:

implicit def asContainer[T](list:MyList[T]): Container[T] = new Container[T] {

    def contains(t:T) = list.size > 0 && (list.head == t || asContainer(list.tail).contains(t))

  }

I am thinking you are conflating subsumption and type (please correct me if you can). The type (without your cast) is MyList[Int] and it has a supertype MyList[Any]. Subsumption only activates when it is necessary to convert the type to match a type parameter which is covariant. In this case the type parameter T on the asContainer method is invariant. The type parameter (rename it A to make this clear) on the trait Container[-A] is contravariant, but it plays no role in the parameter T on the method asContainer.

Thus Vlad's code is not relying on any implementation quirk, rather he is relying on the correct way that typing and subsumption *must* behave in any sane typing system.

A key point is that in any sane static typing system the type is not *only* the subtype, as that would make no sense as we would just write all the types as Any. Normally the source subtype can be assigned to a destination supertype, i.e. subsumption to the destination supertype.

And if a type parameter is covariant then subsumption of the destination supertype can also occur, thus you can arrive at Any. But this subsumption of the destination can only occur if the destination type is a covariant type parameter. This is a fundamental point.

That is why my proposed solution for covariant types is to have two options to direct the subsumption in the case the destination type parameter is covariant:

https://groups.google.com/d/msg/scala-language/B6f-iubR9Mk/OA1h5YU2nSAJ

I believe that will fix all the problems we have with Any! It's so simple and clean.

[Shelby]

On Thursday, September 19, 2013 10:09:47 AM UTC+8, Shelby wrote: 

A key point is that in any sane static typing system the type is not *only* the subtype

s/subtype/supertype/ 

[Paul Phillips]

On Wed, Sep 18, 2013 at 7:09 PM, Shelby <she...@coolpage.com> wrote:

I am thinking you are conflating subsumption and type (please correct me if you can).

FYI the way normal people say this sort of thing is "please correct me if I'm wrong." I'm going to leave you to your theories. Suffice to say I'm happy with the picture I have sketched.

[Shelby]

Apologies I am not an awesome word-smith like you (I live mostly inside my head and somewhat autistic when bringing thoughts out). That is what I meant. I am trying to push us towards consensus. I really don't care about my ego, I just want us to agree on a solution.

How can you say that every type is always an Any? That doesn't make any sense to me. Subsumption only occurs in the presence of a covariant type parameter on a method. As far as I know, it never occurs else where.

Surely we can drill down on that technical point and prove or disprove it? In the interest of being rational and making an objective conclusion.

Nothing personal at all, you know I have recognized you (for example your contribution on virtualized pattern matcher, your rough hack to get unions, etc).

 

[Shelby]

Unfortunately I've discovered that Vlad's solution doesn't provide the correct functionality:

https://groups.google.com/d/msg/scala-language/B6f-iubR9Mk/xBZ8o2TxufgJ

The fix is not to stop any supertypes from qualifying for the input value. Rather that it is desirable, c.f. my reply to JV at the other thread for the reasons. The goal is to stop the subsumption of the *destination* type parameter when the source input value type is neither a supertype nor a subtype-- thus it is not about picking an arbitrary choice for mutual upper bound, rather it is about not subsuming the *destination* type parameter. Once you get a correct conceptualization of the issue then the overall perspective of the problem with Any changes.

And this is where I encourage Paul to have a paradigm shift on his perspective. Paul it appears to me (please correct me if I am wrong) that you want to view this (based on your posts in the above linked thread) as local information that can be decided with a global algorithm. Whereas, I think that is entirely the wrong way to conceptualize what is really going on in the type system.

The key is to recognize that with static typing there is a known type for each reference (and it may reference a subtype) and when assigning from one type to another, only the source type can be subsumed to the destination type. The destination type is never subsumed unless it is a covariant type parameter on a function or method, e.g. include the constructor function.

Thus realize that the notion that all types have a supertype of Any thus they are really Any is the wrong way to conceptualize a static typing system. They can subsume to Any, but they are not Any until they do. And the rules of subsumption are they never subsume if they are the destination type unless the destination type is a covariant parameter.

Thus we can see the only time that subsumption to a mutual upper bound of Any can occur is when the destination type is a covariant parameter. Thus the solution is focus on where that is the case, and selectively turn off the mutual subsumption of the destination covariant type parameter as I have done in my proposed solution.

Never we will want to turn off the subsumption of the source type as that would be the antithesis of subtyping.

The problem again with Vlad's solution is he is turning off subtyping, but in the contravariant direction. The other proposed solutions at SE/SO were turning off subtyping in the covariant direction. None of these are solutions. Only my proposed solution at the above linked thread is.

Hope that makes it clear, now I am really out-the-door (and not going to walk back up the mountain again as I just did to type this).