Type Boundary "Stickyness" on Wildcards

Hi Mathias,

Quoting Mathias :
> Hi Everyone,
>
> I just realized that the Scala compiler does not seem to "carry over"
> type boundaries on wildcards:
>
> scala> class Foo { def foo = 42 }
> defined class Foo
>
> scala> class Bar[A <: Foo](val a: A)
> defined class Bar
>
> scala> def bar(x: Bar[_]) = x.a.foo
> :7: error: value foo is not a member of Any
> def bar(x: Bar[_]) = x.a.foo
>
> I would expect that the parameter of method bar is still upper-bound
> by Foo, even though its exact type parameter is unimportant in the
> method.
> Is there a specific reason for this behavior?

This seems a reasonable expectation since the compiler accepts Bar[_].
However, it looks to me like the compiler shouldn't accept Bar[_] in
the first place. It should require Bar[_ <: Foo].

From the spec:
1) 3.2.10 Bar[_] is equivalent to Bar[T] forSome { type T }
2) 3.2.4 For the parameterized type Bar[T] to be well-formed, T must
conform to the bounds of Bar's type parameter. Here, this means that T
must conform to Foo.
3) 3.5.2 An abstract type conforms to its upper bound. Conformance
is transitive.

From these rules, we can only conclude that T <: Any, not the T <: Foo
that is needed for Bar[T] forSome { type T } to be well-formed.

Your example will compile with an explicit bound:

def bar(x: Bar[_ <: Foo]) = x.a.foo

-Mark

> Cheers,
> Mathias
>
> ---
> mathias [at] decodified [dot] com
> http://www.decodified.com
>
>
>

On Thu, Oct 28, 2010 at 07:25:51PM -0400, Mark Harrah wrote:
> This seems a reasonable expectation since the compiler accepts Bar[_].
> However, it looks to me like the compiler shouldn't accept Bar[_] in
> the first place. It should require Bar[_ <: Foo].

I believe you have been snared by the tricky expansion rules, which the
following may suffice to illustrate. (Or equally likely it will
illustrate that I have no idea what I'm doing or where I am most days.)

scala> def bar(x: Bar[_]) = ()
bar: (x: Bar[_])Unit

// this is the expansion taking place
scala> def bar(x: Bar[T] forSome { type T; }) = ()
bar: (x: Bar[_])Unit

// this is the expansion which would require T to conform to Foo
scala> def bar(x: Bar[T forSome { type T <: Foo; }]) = ()
bar: (x: Bar[T forSome { type T <: Foo }])Unit

// ...and it does require it.
scala> def bar(x: Bar[T forSome { type T; }]) = ()
:7: error: type arguments [T forSome { type T }] do not conform to class Bar's type parameter bounds [A <: Foo]
def bar(x: Bar[T forSome { type T; }]) = ()
^

On Thursday, October 28, 2010 10:54:44 pm Paul Phillips wrote:
> On Thu, Oct 28, 2010 at 07:25:51PM -0400, Mark Harrah wrote:
> > This seems a reasonable expectation since the compiler accepts Bar[_].
> > However, it looks to me like the compiler shouldn't accept Bar[_] in
> > the first place. It should require Bar[_ <: Foo].
>
> I believe you have been snared by the tricky expansion rules, which the
> following may suffice to illustrate. (Or equally likely it will
> illustrate that I have no idea what I'm doing or where I am most days.)

I think I got the expansion right in 1):

1) 3.2.10 Bar[_] is equivalent to Bar[T] forSome { type T }

The question is why is Bar[T] forSome { type T } allowed. I don't see a
conformance rule that can make T <: Foo and therefore make Bar[T] well-formed.

-Mark

> scala> def bar(x: Bar[_]) = ()
> bar: (x: Bar[_])Unit
>
> // this is the expansion taking place
> scala> def bar(x: Bar[T] forSome { type T; }) = ()
> bar: (x: Bar[_])Unit
>
> // this is the expansion which would require T to conform to Foo
> scala> def bar(x: Bar[T forSome { type T <: Foo; }]) = ()
> bar: (x: Bar[T forSome { type T <: Foo }])Unit
>
> // ...and it does require it.
> scala> def bar(x: Bar[T forSome { type T; }]) = ()
> :7: error: type arguments [T forSome { type T }] do not conform to
> class Bar's type parameter bounds [A <: Foo] def bar(x: Bar[T forSome {
> type T; }]) = ()
> ^

On Fri, Oct 29, 2010 at 09:17:36AM -0400, Mark Harrah wrote:
> I think I got the expansion right in 1):
>
> 1) 3.2.10 Bar[_] is equivalent to Bar[T] forSome { type T }

Right, you did: I'm suggesting 2) does not follow from 1).

> The question is why is Bar[T] forSome { type T } allowed. I don't see
> a conformance rule that can make T <: Foo and therefore make Bar[T]
> well-formed.

I have to squeeze my eyes shut and say goodbye to my loved ones before
going up against you in spec reading, but my belief is that

Bar[T] forSome { type T }

is a valid type regardless of what constraints exist on Bar, because it
says only that the type will be some unknown Bar[T]. The space of
unknown Bar[T]s encloses all the valid instantiations: that it encloses
some invalid ones doesn't matter since they won't be instantiable.

I guess it comes down to how you interpret well-formed. Let me see if I
can dredge something more convincing out of the spec.

On Friday, October 29, 2010 09:34:55 am Paul Phillips wrote:
> On Fri, Oct 29, 2010 at 09:17:36AM -0400, Mark Harrah wrote:
> > I think I got the expansion right in 1):
> >
> > 1) 3.2.10 Bar[_] is equivalent to Bar[T] forSome { type T }
>
> Right, you did: I'm suggesting 2) does not follow from 1).
>
> > The question is why is Bar[T] forSome { type T } allowed. I don't see
> > a conformance rule that can make T <: Foo and therefore make Bar[T]
> > well-formed.
>
> I have to squeeze my eyes shut and say goodbye to my loved ones ...

and say 'skolemization' five times...

> ... before
> going up against you in spec reading, but my belief is that
>
> Bar[T] forSome { type T }
>
> is a valid type regardless of what constraints exist on Bar, because it
> says only that the type will be some unknown Bar[T]. The space of
> unknown Bar[T]s encloses all the valid instantiations: that it encloses
> some invalid ones doesn't matter since they won't be instantiable.

This has to come from some rule though. 2) and 3) were the rules I understood
to be relevant.

> I guess it comes down to how you interpret well-formed. Let me see if I
> can dredge something more convincing out of the spec.

Taking our type:
Bar[T] forSome { type T }

and breaking it down, we have:
ExistentialType ::= InfixType forSome { TypeDecl }

Merging a few levels, our InfixType is a ParameterizedType:
ParameterizedType ::= StableId '[' StableId ']'

This parameterized type, Bar[T], must be well-formed according to 3.2.4. It
says "the parameterized type is well-formed if each actual type parameter
conforms to its bounds ...". The enclosing existential type binds the type
variable T. Then we apply the conformance rule for type variables and try to
get T <: Foo, but I don't see how that is possible.

What I was trying to show is that Bar[T] is a parameterized type within the
existential type that still has to follow the well-formedness rule. Sorry if
you already understood that that is what I was saying.

-Mark

On Fri, Oct 29, 2010 at 10:09:44AM -0400, Mark Harrah wrote:
> and say 'skolemization' five times...

I will, actually.

3.5.2: The existential type T forSome { Q } conforms to U if its
skolemization conforms to U.

3.2.10: A skolemization of T forSome { Q } is a type instance ... where
each ti' is a fresh abstract type with lower bound omega-Li and upper
bound omega-Ui.

I read this to mean that the bounds as defined in Bar are introduced in
skolemization, and therefore the existential conforms without them.

On Friday, October 29, 2010 12:12:33 pm Paul Phillips wrote:
> On Fri, Oct 29, 2010 at 10:09:44AM -0400, Mark Harrah wrote:
> > and say 'skolemization' five times...
>
> I will, actually.
>
> 3.5.2: The existential type T forSome { Q } conforms to U if its
> skolemization conforms to U.

I don't think this rule matters here. We don't care what the full existential
type Bar[X] forSome { type X } conforms to. We care what X conforms to
because we require that for the parameterized type Bar[X], X conforms to Foo.

> 3.2.10: A skolemization of T forSome { Q } is a type instance ... where
> each ti' is a fresh abstract type with lower bound omega-Li and upper
> bound omega-Ui.
>
> I read this to mean that the bounds as defined in Bar are introduced in
> skolemization, and therefore the existential conforms without them.

The bounds of Q (here, T >: Nothing <: Any) are what are used in
skolemization. Here, it means something like:

type X >: Nothing <: Any
Bar[X]

rather than:
type X >: Nothing <: Foo
Bar[X]

-Mark

Gentlemen,

after having thought about this a bit more (and without wanting to interrupt your spec exegesis) I would like to take a step back and propose an explanation, why, IMHO, the current compiler behavior makes sense.

Suppose the compiler _would_ carry over the type bound to Bar[_]. Originally I deemed this a good idea because it would allow my code to be more DRY since I would only have to specify the type bound once and not at every (wildcard) usage site sprinkled around my code base.
However, if the compiler did this for Bar[_], for consistency reasons it would also have to do it for Bar[A]. The latter however would have some strange consequences.

def bar[A](x: Bar[A], y: Bob[A])

for example would suddenly have to carry an implicit type bound for Bob. If Bob had its own type bound things would be really messy.

So clearly, automatic type bound carry over does not really make sense.

But why does the compiler accept Bar[_] and not only Bar[_ <: Foo]?
I suppose because the respective code might not actually require the type bound.
If all I want to do is call "toString" for example I probably should not be required to state the type bound.

So, even without looking at the SLS, the current behavior does make sense to me.

Cheers,
Mathias

---
mathias [at] decodified [dot] com
http://www.decodified.com

On 29.10.2010, at 18:12, Paul Phillips wrote:

> On Fri, Oct 29, 2010 at 10:09:44AM -0400, Mark Harrah wrote:
>> and say 'skolemization' five times...
>
> I will, actually.
>
> 3.5.2: The existential type T forSome { Q } conforms to U if its
> skolemization conforms to U.
>
> 3.2.10: A skolemization of T forSome { Q } is a type instance ... where
> each ti' is a fresh abstract type with lower bound omega-Li and upper
> bound omega-Ui.
>
> I read this to mean that the bounds as defined in Bar are introduced in
> skolemization, and therefore the existential conforms without them.
>

On Fri, Oct 29, 2010 at 01:29:45PM -0400, Mark Harrah wrote:
> I don't think this rule matters here. We don't care what the full
> existential type Bar[X] forSome { type X } conforms to. We care what
> X conforms to because we require that for the parameterized type
> Bar[X], X conforms to Foo.

As you must already know, I'm not coming at this from a position of
authority: rather I have reason to believe the current behavior is
intended and I'm attempting to retrofit a believable explanation.
Sometimes you stumble on the truth that way but so far you're not taking
the bait, which isn't promising for the outcome of that lottery. So I
will table this argument until I actually believe what I'm saying (or
better yet, disbelieve it.)

On the plus side I'm finally reading the spec cover to cover. I had no
idea the complete lyrics to "yellow submarine" were in the
specification! Yet I have to admit, in context it was hard to see any
other way that section could have been written.