[scala] Re: Unsoundness in higher-order type parameters?

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@...> 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@...> 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