subtyping of method types

119 views
Skip to first unread message

Lukas Rytz

unread,
Nov 19, 2012, 8:17:37 AM11/19/12
to scala-i...@googlegroups.com
Given two method types (ts: Ts): R  and  (ts': Ts'): R'  the conformance relation says that the
argument types have to be the same (instead of contravariant subtyping)

Is that due to the JVM?


scala> if (x) new { def foo(a: String) = 1 } else new { def foo(a: Object) = 2 }
res4: Object = $anon$2@1a2f9dd


In principle the type could be   Object { def foo(a: String): Int }

Thanks,
Lukas

martin odersky

unread,
Nov 19, 2012, 9:05:33 AM11/19/12
to scala-internals
On Mon, Nov 19, 2012 at 2:17 PM, Lukas Rytz <lukas...@epfl.ch> wrote:
Given two method types (ts: Ts): R  and  (ts': Ts'): R'  the conformance relation says that the
argument types have to be the same (instead of contravariant subtyping)

Is that due to the JVM?


In a sense (or maybe more than one), yes. JVM needs the precise argument type for the dispatching. Moreover, combining contravariant method argument typing with overloading leads to some severe headaches.

Cheers

 - Martin

 
scala> if (x) new { def foo(a: String) = 1 } else new { def foo(a: Object) = 2 }
res4: Object = $anon$2@1a2f9dd


In principle the type could be   Object { def foo(a: String): Int }

Thanks,
Lukas



--
Martin Odersky
Prof., EPFL and Chairman, Typesafe
PSED, 1015 Lausanne, Switzerland
Tel. EPFL: +41 21 693 6863
Tel. Typesafe: +41 21 691 4967

Simon Ochsenreither

unread,
Nov 19, 2012, 1:34:15 PM11/19/12
to scala-i...@googlegroups.com
I also wondered about that some time ago: http://stackoverflow.com/questions/8160570/are-there-statically-typed-programming-languages-with-inheritance-where-method-p

Except for the obvious overloading issues, I never got a great answer. I think the hint with OCaml could be interesting, though.

Maybe Cardelli has anything about it?

Paul Phillips

unread,
Nov 19, 2012, 2:29:01 PM11/19/12
to scala-i...@googlegroups.com
Here's an answer I wrote in private email a couple weeks ago.

                                                                                                                                                                                                                                                               
Date: Sat, 10 Nov 2012 18:50:39 -0700
Subject: Re: [scala-user] Overrides with contra-variant parameter types?
From: Paul Phillips <pa...@improving.org>
To: "Peter C. Chapin" <PCh...@vtc.vsc.edu>

[I'm not on scala-user; you can forward this if you like.]

On Sat, Nov 10, 2012 at 1:40 PM, Peter C. Chapin <PCh...@vtc.vsc.edu>wrote:

> Okay, so it's a restriction imposed by the platform. Fair enough!
>

It is not a restriction imposed by the platform. One could implement
overrides with contravariant refinement in a manner exactly analogous to
the way covariant refinement is already done.

scala> class A { def f(): Object = ??? } ; class B extends A { override def
f(): String = ??? } ;
  classOf[B].getDeclaredMethods.map(_.toGenericString).foreach(println)
public java.lang.Object $line4.$read$$iw$$iw$B.f()
public java.lang.String $line4.$read$$iw$$iw$B.f()

Notice there are two f() methods in B: one with the declared signature, and
one with the signature of the overridden method. This is what bridge
methods are for. In a hypothetical contravariant refinement:

scala> class A { def f(s: String): Unit = ??? } ; class B extends A {
override def f(s: Object): Unit = ??? }

You would find both (String)Unit and (Object)Unit signatures in B, with the
former forwarding to the latter.

A more realistic reason why this isn't done is that it would introduce
tremendous ambiguity, and it would be very difficult to incorporate into
overloading resolution without creating surprises. If you override an
overloaded method with a more general parameter type, you could easily make
one of the inherited overloads "more specific" for a set of parameter types
than the same call would be when the receiver has the static type of the
superclass. There would also have to be some facility for specifying which
method you are overriding, since any method with the same name and arity
and more specific parameters might be the override target - and there could
be arbitrarily many.

It's very unlikely it would be a net win, though I see the appeal from a
theoretical/consistency standpoint.

Lukas Rytz

unread,
Nov 20, 2012, 5:26:57 AM11/20/12
to scala-i...@googlegroups.com
The reason I ask is interaction with dependent method types, singleton types. /cc @adriaanm


Assume we had contravariant method subtyping. Given types B <: A <: Object, the following should hold

  (x': A)(y': B)T  <:  (x: B)(y: x.type)T

the lefthand type accepts larger argument types, so it's more specific. Now, the current implementation
for method types does the following:

  matchingParams(params1, params2) &&   // here we'd check contravariant subtyping, instead of equivalence
  isSubType(res1, res2.substSym(params2, params1))

So the compiler replaces the parameter symbols in the supertype by the ones of the subtype, and we get
the following test for the result types

   (y': B)T   <:   (y: x'.type)T

This test fails, because   x'.type <: B    ===>   A <: B   fails.

If we replaced symbols the other way around, it would have worked in this case. Now, I don't know if it's
good enough to just replace symbols the other way around, or if that can also fail in some cases. I tried
to find a counter-example, but could not. Check the following:

  (x': A)x'.type  <:  (x: B)B

This subtyping statement is in fact true, even though that's non-intuitive at first. Obviously the argument
types are fine, the subtype accepts a larger argument type. It seems at first that the return types would
not conform, because if you expand   x'.type <: B   to   A <: B   that fails. Indeed, the lefthand type could
return an A, while the righthand type guarantees to always return a B.

HOWEVER, assume you have a function of the lefthand type

  f: (x': A)x.type   // note: it can only return the value that it receives as argument

If you are up-casting that function to the righthand type   (x: B)B   what happens? Now you cannot anymore
pass an argument of type  A  into the function, you have to give it a B. And since the function will always
return the same value as the one you pass into it, you will also get back a B. So the function   f   satisfies
the contract of type   (x: B)B.

So the subtyping implementation would do the following, which seems correct



                        B <: B
                    -------------  // expand the singleton to the underlying
                     x.type <: B
              -----------------------
  B <: A      (x'.type)[x' -> x] <: B
----------------------------------------
    (x': A)x'.type  <:  (x: B)B



Thoughts? Anybody knows papers on the subject?
Lukas

Adriaan Moors

unread,
Nov 20, 2012, 2:16:18 PM11/20/12
to scala-i...@googlegroups.com
1) on the substSym question, I don't know why it's this way around
I agree your reasoning makes sense -- this is how dependently typed calculi with subtyping deal with function types


2) I think the problem with overloading/overriding+contravariance may be related to the answer here: http://stackoverflow.com/questions/2995926/why-is-there-no-parameter-contra-variance-for-overriding

suppose we allow contravariance for method arguments in overriding (dynamic dispatch) and overloading (static dispatch)

class Top
class Derived extends Top

class A {
  def foo(x: Top) = println("top")
  def foo(x: Derived) = println("derived")
}

class B extends A {
  // where should the super call go if we allow contra-variant overriding?
  // I guess you could say "the most-specific overload"
  override def foo(x: Derived) = {println("more"); super.foo(x)}
}

Paul Phillips

unread,
Nov 20, 2012, 2:25:01 PM11/20/12
to scala-i...@googlegroups.com


On Tue, Nov 20, 2012 at 11:16 AM, Adriaan Moors <adriaa...@typesafe.com> wrote:
  // where should the super call go if we allow contra-variant overriding?

That's why I said in my other email we'd have to devise some mechanism for specifying it; like super[Foo].bar, except [Foo] has to specify which method overload, not which parent. Messy to be sure.

Lukas Rytz

unread,
Nov 20, 2012, 3:07:36 PM11/20/12
to scala-i...@googlegroups.com
On Tue, Nov 20, 2012 at 8:16 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:
1) on the substSym question, I don't know why it's this way around

It doesn't matter in scala because we don't do contravariant subtyping for functions. However
I wonder if we don't have a similar problem with type parameters (where we do a similar symbol
substitution), but I didn't have time yet to think about it enough.

 
I agree your reasoning makes sense -- this is how dependently typed calculi with subtyping deal with function types

Will look at that, thanks.

Lukas Rytz

unread,
Nov 21, 2012, 8:42:17 AM11/21/12
to scala-i...@googlegroups.com
On Tue, Nov 20, 2012 at 8:16 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:
1) on the substSym question, I don't know why it's this way around
I agree your reasoning makes sense -- this is how dependently typed calculi with subtyping deal with function types


For reference, here's a relevant piece from the paper (they use A' not A for the type of x)

Inline image 2
The subtyping rule for π-types, (s-π), is contravariant in the domain and covariant in the codomain; the codomains are compared under the stronger restriction that x : A′. Because of this the final judgement is needed to ensure that πx:A. B is indeed a well-formed type.


Paolo G. Giarrusso

unread,
Nov 23, 2012, 7:22:25 PM11/23/12
to scala-i...@googlegroups.com
Il giorno martedì 20 novembre 2012 21:08:03 UTC+1, Lukas Rytz ha scritto:


On Tue, Nov 20, 2012 at 8:16 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:
1) on the substSym question, I don't know why it's this way around

It doesn't matter in scala because we don't do contravariant subtyping for functions.
 
Functions have contravariant subtyping; Scala "just" lacks dependent function types (you can encode first-class dependent functions, but not in general, and they won't be subtypes of FunctionX).
 
However
I wonder if we don't have a similar problem with type parameters (where we do a similar symbol
substitution), but I didn't have time yet to think about it enough.

 
I agree your reasoning makes sense -- this is how dependently typed calculi with subtyping deal with function types

I'm a bit concerned that the solution is not part of DOT rules - it seems that it's not part because such a type is not directly expressible. In your FOOL 2012 paper, figure 5, rule MDECL-WF doesn't seem to provide for dependent method types (skimming the Scalina paper doesn't offer immediate help, I'll need to study it more carefully).

martin odersky

unread,
Nov 24, 2012, 3:32:44 AM11/24/12
to scala-internals
On Sat, Nov 24, 2012 at 1:22 AM, Paolo G. Giarrusso <p.gia...@gmail.com> wrote:
Il giorno martedì 20 novembre 2012 21:08:03 UTC+1, Lukas Rytz ha scritto:



On Tue, Nov 20, 2012 at 8:16 PM, Adriaan Moors <adriaa...@typesafe.com> wrote:
1) on the substSym question, I don't know why it's this way around

It doesn't matter in scala because we don't do contravariant subtyping for functions.
 
Functions have contravariant subtyping; Scala "just" lacks dependent function types (you can encode first-class dependent functions, but not in general, and they won't be subtypes of FunctionX).
 
However
I wonder if we don't have a similar problem with type parameters (where we do a similar symbol
substitution), but I didn't have time yet to think about it enough.

 
I agree your reasoning makes sense -- this is how dependently typed calculi with subtyping deal with function types

I'm a bit concerned that the solution is not part of DOT rules - it seems that it's not part because such a type is not directly expressible. In your FOOL 2012 paper, figure 5, rule MDECL-WF doesn't seem to provide for dependent method types (skimming the Scalina paper doesn't offer immediate help, I'll need to study it more carefully).
 

I believe dependent method types can be encoded in an extension of DOT where concrete trait members can be defined:

  def m(x: S): x.T = expr

becomes

  trait mC {
     val x: S
     def result: x.T = expr
   }

And

  m(arg)

becomes new mC { val x = arg }.result

This does not give us dependent function types (since classes cannot be passed as arguments), but Scala does not have dependent function types either. Note also that this construction does not give us contravariance in the argument type, so it matches Scala instead of the standard dependently typed calculi.

Of course, in Scala the programming language we'd still have dependent method types; my construction simply showed that they do not add anything fundamental.

Cheers

 - Martin
Reply all
Reply to author
Forward
0 new messages