Unsoundness in higher-order type parameters?

Hi Vladimir,
I think this is ok. The kind of _ in _[X, Y <: X] is (X: *) -> *(Nothing, X) -> * The kind of _ in _[X, Y] is * -> * -> *Now, * -> * -> * is a subkind of (X: *) -> *(Nothing, X) -> * , just like Any -> Any -> Any is a subtype of Any -> String -> Any.
Or am I missing something?

cheers,adriaan
On Tue, Jun 16, 2009 at 2:31 PM, Vladimir Reshetnikov <v.reshetnikov@gmail.com> wrote:

Hi,

Consider these definitions:

///////////////////////////////////////
trait A[B[_[X, Y <: X]]] {
 def f() : B[P]
}

trait C[_[X, Y]]

trait P[X, Y <: X]
///////////////////////////////////////

Type application C[P] is (correctly) rejected by the Scala 2.7.5
compiler. But A[C] is (incorrectly) accepted, which results in
incorrect type of member f(). It looks like unsoundness.

Thanks,
Vladimir


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

Hi Adriaan,

Let us give names to all type parameters:

///////////////////////////////////////
trait A[B[D[X, Y <: X]]] {
def f() : B[P]
}

trait C[E[T, S]]

trait P[U, V <: U]
///////////////////////////////////////

Now, the kinds are:

D : X@* -> *(Nothing,X) -> *
B : (X@* -> *(Nothing,X) -> *) -> *

E : * -> * -> *
C : (* -> * -> *) -> *

In type application A[C], C is substituted instead of the type parameter B.
So (* -> * -> *) -> * must be a subkind of (X@* -> *(Nothing,X) -> *) -> *.
Contravariantly, X@* -> *(Nothing,X) -> * must be a subkind of * -> * -> *.
Contravariantly, * must be a subkind of *(Nothing,X), but this is not
the case. So, this application is ill-typed. As I wrote before, it
demonstrates itself in the ill-kinded type application C[P] in the
return type of f().

Thanks,
Vladimir

On 6/17/09, Adriaan Moors wrote:
> Hi Vladimir,
> I think this is ok. The kind of _ in _[X, Y <: X] is (X: *) -> *(Nothing,
> X)
> -> *
> The kind of _ in _[X, Y] is * -> * -> *
> Now, * -> * -> * is a subkind of (X: *) -> *(Nothing, X) -> * , just like
> Any -> Any -> Any is a subtype of Any -> String -> Any.
>
> Or am I missing something?
>
> cheers,
> adriaan
>
> On Tue, Jun 16, 2009 at 2:31 PM, Vladimir Reshetnikov <
> v.reshetnikov@gmail.com> wrote:
>
>> Hi,
>>
>> Consider these definitions:
>>
>> ///////////////////////////////////////
>> trait A[B[_[X, Y <: X]]] {
>> def f() : B[P]
>> }
>>
>> trait C[_[X, Y]]
>>
>> trait P[X, Y <: X]
>> ///////////////////////////////////////
>>
>> Type application C[P] is (correctly) rejected by the Scala 2.7.5
>> compiler. But A[C] is (incorrectly) accepted, which results in
>> incorrect type of member f(). It looks like unsoundness.
>>
>> Thanks,
>> Vladimir
>>
>>
>> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
>>
>

Ouch. You're right. I'll file this one myself ;-)
adriaan

On Wed, Jun 17, 2009 at 3:57 PM, Vladimir Reshetnikov <v.reshetnikov@gmail.com> wrote:

Hi Adriaan,

Let us give names to all type parameters:

///////////////////////////////////////
trait A[B[D[X, Y <: X]]] {
 def f() : B[P]
}

trait C[E[T, S]]

trait P[U, V <: U]
///////////////////////////////////////

Now, the kinds are:

D : X@* -> *(Nothing,X) -> *
B : (X@* -> *(Nothing,X) -> *) -> *

E : * -> * -> *
C : (* -> * -> *) -> *

In type application A[C], C is substituted instead of the type parameter B.
So (* -> * -> *) -> * must be a subkind of (X@* -> *(Nothing,X) -> *) -> *.
Contravariantly, X@* -> *(Nothing,X) -> * must be a subkind of * -> * -> *.
Contravariantly, * must be a subkind of *(Nothing,X), but this is not
the case. So, this application is ill-typed. As I wrote before, it
demonstrates itself in the ill-kinded type application C[P] in the
return type of f().

Thanks,
Vladimir

On 6/17/09, Adriaan Moors <adriaan.moors@cs.kuleuven.be> wrote:
> Hi Vladimir,
> I think this is ok. The kind of _ in _[X, Y <: X] is (X: *) -> *(Nothing,
> X)
> -> *
> The kind of _ in _[X, Y] is * -> * -> *
> Now, * -> * -> * is a subkind of (X: *) -> *(Nothing, X) -> * , just like
> Any -> Any -> Any is a subtype of Any -> String -> Any.
>
> Or am I missing something?
>
> cheers,
> adriaan
>
> On Tue, Jun 16, 2009 at 2:31 PM, Vladimir Reshetnikov <
> v.reshetnikov@gmail.com> wrote:
>
>> Hi,
>>
>> Consider these definitions:
>>
>> ///////////////////////////////////////
>> trait A[B[_[X, Y <: X]]] {
>>  def f() : B[P]
>> }
>>
>> trait C[_[X, Y]]
>>
>> trait P[X, Y <: X]
>> ///////////////////////////////////////
>>
>> Type application C[P] is (correctly) rejected by the Scala 2.7.5
>> compiler. But A[C] is (incorrectly) accepted, which results in
>> incorrect type of member f(). It looks like unsoundness.
>>
>> Thanks,
>> Vladimir
>>
>>
>> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
>>
>


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

Vladimir, All,
I've implemented a new approach for kind inference and subkinding, which should address the issues that you discovered.
It's not ready yet to go into trunk -- I would greatly appreciate your help in testing the new code (please git pull them from http://github.com/adriaanm/scala/tree/explicitkinds), so that I can try to still get it in in time for 2.8.
Please note that I haven't fixed the issues with refinement types yet -- that's not my area (but I'll have a look soon)
cheers,adriaan

On Wed, Jun 17, 2009 at 4:39 PM, Adriaan Moors <adriaan.moors@cs.kuleuven.be> wrote:

Ouch. You're right. I'll file this one myself ;-)
adriaan

On Wed, Jun 17, 2009 at 3:57 PM, Vladimir Reshetnikov <v.reshetnikov@gmail.com> wrote:

Hi Adriaan,

Let us give names to all type parameters:

///////////////////////////////////////
trait A[B[D[X, Y <: X]]] {
 def f() : B[P]
}

trait C[E[T, S]]

trait P[U, V <: U]
///////////////////////////////////////

Now, the kinds are:

D : X@* -> *(Nothing,X) -> *
B : (X@* -> *(Nothing,X) -> *) -> *

E : * -> * -> *
C : (* -> * -> *) -> *

In type application A[C], C is substituted instead of the type parameter B.
So (* -> * -> *) -> * must be a subkind of (X@* -> *(Nothing,X) -> *) -> *.
Contravariantly, X@* -> *(Nothing,X) -> * must be a subkind of * -> * -> *.
Contravariantly, * must be a subkind of *(Nothing,X), but this is not
the case. So, this application is ill-typed. As I wrote before, it
demonstrates itself in the ill-kinded type application C[P] in the
return type of f().

Thanks,
Vladimir

On 6/17/09, Adriaan Moors <adriaan.moors@cs.kuleuven.be> wrote:
> Hi Vladimir,
> I think this is ok. The kind of _ in _[X, Y <: X] is (X: *) -> *(Nothing,
> X)
> -> *
> The kind of _ in _[X, Y] is * -> * -> *
> Now, * -> * -> * is a subkind of (X: *) -> *(Nothing, X) -> * , just like
> Any -> Any -> Any is a subtype of Any -> String -> Any.
>
> Or am I missing something?
>
> cheers,
> adriaan
>
> On Tue, Jun 16, 2009 at 2:31 PM, Vladimir Reshetnikov <
> v.reshetnikov@gmail.com> wrote:
>
>> Hi,
>>
>> Consider these definitions:
>>
>> ///////////////////////////////////////
>> trait A[B[_[X, Y <: X]]] {
>>  def f() : B[P]
>> }
>>
>> trait C[_[X, Y]]
>>
>> trait P[X, Y <: X]
>> ///////////////////////////////////////
>>
>> Type application C[P] is (correctly) rejected by the Scala 2.7.5
>> compiler. But A[C] is (incorrectly) accepted, which results in
>> incorrect type of member f(). It looks like unsoundness.
>>
>> Thanks,
>> Vladimir
>>
>>
>> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
>>
>


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm

Vladimir, All,
I've implemented a new approach for kind inference and subkinding, which should address the issues that you discovered.
It's not ready yet to go into trunk -- I would greatly appreciate your help in testing the new code (please git pull them from http://github.com/adriaanm/scala/tree/explicitkinds), so that I can try to still get it in in time for 2.8.
Please note that I haven't fixed the issues with refinement types yet -- that's not my area (but I'll have a look soon)
cheers,adriaan

On Wed, Jun 17, 2009 at 4:39 PM, Adriaan Moors <adriaan.moors@cs.kuleuven.be> wrote:

Ouch. You're right. I'll file this one myself ;-)
adriaan

On Wed, Jun 17, 2009 at 3:57 PM, Vladimir Reshetnikov <v.reshetnikov@gmail.com> wrote:

Hi Adriaan,

Let us give names to all type parameters:

///////////////////////////////////////
trait A[B[D[X, Y <: X]]] {
 def f() : B[P]
}

trait C[E[T, S]]

trait P[U, V <: U]
///////////////////////////////////////

Now, the kinds are:

D : X@* -> *(Nothing,X) -> *
B : (X@* -> *(Nothing,X) -> *) -> *

E : * -> * -> *
C : (* -> * -> *) -> *

In type application A[C], C is substituted instead of the type parameter B.
So (* -> * -> *) -> * must be a subkind of (X@* -> *(Nothing,X) -> *) -> *.
Contravariantly, X@* -> *(Nothing,X) -> * must be a subkind of * -> * -> *.
Contravariantly, * must be a subkind of *(Nothing,X), but this is not
the case. So, this application is ill-typed. As I wrote before, it
demonstrates itself in the ill-kinded type application C[P] in the
return type of f().

Thanks,
Vladimir

On 6/17/09, Adriaan Moors <adriaan.moors@cs.kuleuven.be> wrote:
> Hi Vladimir,
> I think this is ok. The kind of _ in _[X, Y <: X] is (X: *) -> *(Nothing,
> X)
> -> *
> The kind of _ in _[X, Y] is * -> * -> *
> Now, * -> * -> * is a subkind of (X: *) -> *(Nothing, X) -> * , just like
> Any -> Any -> Any is a subtype of Any -> String -> Any.
>
> Or am I missing something?
>
> cheers,
> adriaan
>
> On Tue, Jun 16, 2009 at 2:31 PM, Vladimir Reshetnikov <
> v.reshetnikov@gmail.com> wrote:
>
>> Hi,
>>
>> Consider these definitions:
>>
>> ///////////////////////////////////////
>> trait A[B[_[X, Y <: X]]] {
>>  def f() : B[P]
>> }
>>
>> trait C[_[X, Y]]
>>
>> trait P[X, Y <: X]
>> ///////////////////////////////////////
>>
>> Type application C[P] is (correctly) rejected by the Scala 2.7.5
>> compiler. But A[C] is (incorrectly) accepted, which results in
>> incorrect type of member f(). It looks like unsoundness.
>>
>> Thanks,
>> Vladimir
>>
>>
>> Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm
>>
>


Disclaimer: http://www.kuleuven.be/cwis/email_disclaimer.htm