English 中文(简体)
Where s the contravariance?
原标题:

A canonical example of patching up an otherwise covariant class is as follows:

abstract class Stack[+A] {
  def push[B >: A]( x: B ) : Stack[B]
  def top: A
  def pop: Stack[A]

Now, if I remove the implicit covariance and manually annotate the class, I get this:

abstract class Stack[A] {
  def push[B >: A]( x: B ) : Stack[B]
  def top [B >: A]: B
  def pop [B >: A]: Stack[B]
  def cast[B >: A]: Stack[B]
}

(Quick correctness proof: a Stack[A] has elements of type A, so if B is more permissive we can always return an A in place of B. Similarly, given any stack of A, we can use it in place of a stack of B if B can accept A.)

But now I m a little confused: there should be contravariance somewhere here, but all of the subtype relations here seem to be the same. What happened?

To elaborate anymore, we define a contravariant functor F such that (a -> b) -> (F b -> F a). In particular, the functor F a on a -> r is contravariant, as (a -> b) -> ((b -> r) -> (a -> r)) simply by composing the functions. From a formalism perspective, I expect arrows to be flipping. So from a purely syntactic perspective, I get confused when no arrows are flipping (but there should be!) Is my annotated way of writing the Scala simply a "natural" representation of the contravariance of functions, such that you don’t even notice it? Is my abstract class wrong? Is there something misleading about the second presentation?

最佳回答

You re looking at the same relationship. Let s think about what Stack[+A] means: if C is a subclass of A, then Stack[C] is treated as a subclass of Stack[A], i.e., it can fill in for class A anywhere; with all methods annotated with superset generics, this is of course true, as you have pointed out.

But you haven t designed your original class to make the argument of push be in the contravariant position. These relations naturally arise when you impose restrictions on what you can handle--then, if a subclass means that the method can handle less, C[Subclass] acts as a superclass of C[Original] since C[Original] can handle everything that the subclass can handle (and more). But push can handle anything the way you ve defined it.

So this is exactly how type bounds and variance interact: if you allow type widening in exactly those spots that are in contravariant position (i.e. which would otherwise restrict you), then you are allowed to be covariant. Otherwise you must be invariant or contravariant. (Pop doesn t allow you to be contravariant, so you d have to be invariant. See, for example, the mutable collections, where invariance is the norm for exactly this reason--you re not free to widen the type on push.)

问题回答

暂无回答




相关问题
Are there type signatures which Haskell can t verify?

This paper establishes that type inference (called "typability" in the paper) in System F is undecidable. What I ve never heard mentioned elsewhere is the second result of the paper, namely that "type ...

Where s the contravariance?

A canonical example of patching up an otherwise covariant class is as follows: abstract class Stack[+A] { def push[B >: A]( x: B ) : Stack[B] def top: A def pop: Stack[A] Now, if I remove the ...

Books for beginning type system theory [closed]

I want to study type system theory. I don t have any background in type system theory so I m more or less a beginner (except the articles I ve read on the subject and which I find intimidating because ...

Typing the Y combinator

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html is a concise definition of the simply typed lambda calculus in Prolog. It looks okay, but then he purports to ...

A question about logic and the Curry-Howard correspondence

Could you please explain me what is the basic connection between the fundamentals of logical programming and the phenomenon of syntactic similarity between type systems and conventional logic?

热门标签