kmizuさんとpaulpさんのやりとり

Paul Phillips 💙 @contrarivariant

@kmizu that is a logical thing to think, but nope.

Paul Phillips 💙 @contrarivariant

@kmizu martin: “Same-named inner classes which are in no relationship with each other are explicitly allowed in both Java and Scala.”

kmizu @kmizu

@extempore2 Hi. It seems that you example doesn't indicate unsoundness of Scala's type system but scalac's bug for me.

Paul Phillips 💙 @contrarivariant

@kmizu https://t.co/TtbL14sa7Z

Paul Phillips 💙 @contrarivariant

@kmizu More at https://t.co/QlGqn3yINU

kmizu @kmizu

@extempore2 .@kmizu Of course. Scala's type system doesn't have formal definition. However, many practical languages doesn't have it, too.

kmizu @kmizu

@extempore2 Thanks. I'l see your pointer at first.

Paul Phillips 💙 @contrarivariant

@kmizu See also https://t.co/o0vgOGNcrb

kmizu @kmizu

@extempore2 What do you mean? I see think the problem is whether Scala type system is unsound or not.

Paul Phillips 💙 @contrarivariant

@kmizu I don’t think there’s any question as to whether it is unsound. It is.

Paul Phillips 💙 @contrarivariant

@kmizu Did you read my comments in https://t.co/EbHGw26SDj ?

kmizu @kmizu

@extempore2 .@kmizu And it is not determined completely unless the type system is not well-defined.

Paul Phillips 💙 @contrarivariant

@kmizu I am not sure what “it” refers to in “it is not determined completely.”

kmizu @kmizu

@extempore2 Yes, of course. But the unsoundness is not trivial for me, at least.

Paul Phillips 💙 @contrarivariant

@kmizu I am not sure how one should judge unsoundness to be trivial.

kmizu @kmizu

@extempore2 I'm sorry for not good at English. "it" refers "whether Scala type system is unsound or not".

Paul Phillips 💙 @contrarivariant

@kmizu Here is another one, which includes a huge number of classes. https://t.co/pkxn11Yen8

Paul Phillips 💙 @contrarivariant

@kmizu As specified it is unquestionably unsound. This is openly admitted by martin in SI-7255. But there is lots more.

kmizu @kmizu

@extempore2 OK. I understood what you want to say at last. Certainly, the problem https://t.co/WSly8iSFIZ indicates unsoundenss. Thanks.

Paul Phillips 💙 @contrarivariant

@kmizu Thanks for investigating.

kmizu @kmizu

@extempore2 I have another question. How do you think about DOT? According to Martin, The DOT (Dependend Object Types) fixes the problem.

kmizu @kmizu

@extempore2 .@kmizu I'd already read the Namin's paper about DOT, of course.

Paul Phillips 💙 @contrarivariant

@kmizu The soundness issues in scala are not a result of the theory but of indifference to correctness. DOT can’t fix that.

kmizu @kmizu

@extempore2 Yes, DOT can'T fix scalac's implementation. However, the different type theory Scala is based on can fix future's implementation

Paul Phillips 💙 @contrarivariant

@kmizu No theory yet devised can outrun indifference to correctness.