From 25a445ef875b2e34bbe4e8239a8f7110b123b5f6 Mon Sep 17 00:00:00 2001 From: clhodapp Date: Fri, 14 Feb 2014 15:59:52 -0600 Subject: Add an extremely well-commented test This commit includes a test for some simple existential subtyping checks. It is exceptionally well-commented and may be helpful to someone trying to figure out what the rules are (supposed to be) in the future. --- test/files/neg/literate_existentials.check | 4 + test/files/neg/literate_existentials.scala | 224 +++++++++++++++++++++++++++++ 2 files changed, 228 insertions(+) create mode 100644 test/files/neg/literate_existentials.check create mode 100644 test/files/neg/literate_existentials.scala (limited to 'test/files') diff --git a/test/files/neg/literate_existentials.check b/test/files/neg/literate_existentials.check new file mode 100644 index 0000000000..c98f976f79 --- /dev/null +++ b/test/files/neg/literate_existentials.check @@ -0,0 +1,4 @@ +literate_existentials.scala:189: error: Cannot prove that Int <:< M forSome { type M <: String }. + implicitly[Int <:< (M forSome { type M >: Nothing <: String })] // fails + ^ +one error found diff --git a/test/files/neg/literate_existentials.scala b/test/files/neg/literate_existentials.scala new file mode 100644 index 0000000000..8580347bf9 --- /dev/null +++ b/test/files/neg/literate_existentials.scala @@ -0,0 +1,224 @@ + +object LiterateExistentials { + +// Let's play with Scala's type system a bit. +// +// From adriaanm, we have the following substitution rule, which allows us to +// determine whether a type is a subtype of an existential in Scala: +// +// +// T <: subst(U) for all i: subst(Li) <: Vi /\ Vi <: subst(Hi) +// -------------------------------------------------------------- +// T <: U forSome {type X1 :> L1 <: H1; ...; type Xn :> Ln <: Hn} +// +// where subst(T) = T.subst(Xi, Vi) // Vi fresh type variables +// +// T is a subtype of some existential if all constraints of the existential hold +// after substituting Vi for the existentially quantified type variables Xi, +// and T is a subtype of the underlying type U with the same substitution applied. +// +// +// Since we are not a formal substitution system, we will actually be using +// this rule 'backward' in order to determine whether it allows us to +// truthfully make claims; In each example, we will start with the proposition +// that a type is a subtype of an existential. Then, we will fit the +// proposition into the form on the bottom rule by creating a set of bindings +// which allow one to be transformed into the other. Next, we will express the +// top of the substitution rule in terms of a series of constraints. We will +// simplify those constraints until simple inspection can determine whether +// they are consistent. From this, we can conclude whether the type system / +// environment admit the top of the substitution rule (and thus, the bottom). If +// they do, we can say that the proposition is true. + + +// In each case, we will also probe the compiler to see whether _it_ thinks that +// the proposition holds, using an uncommented implicitly[_ <:< _] line. + + + + +// Proposition: Nothing :< (A forSome { type A >: String <: Any }) +// +// +// Bindings: +// T := Nothing +// U := A +// X1 := A +// L1 := String +// H1 := Any +// +// We need: +// +// Nothing <: V1 // (U, which is "A", which V1 substituted for all instances of A) +// String <: V1 +// V1 <: Any +// +// Which simplify to: +// V1 >: String <: Any +// +// That's not inconsistent, so we can say that: +// T <: U forSome { type X1 >: L1 <: H1 } +// which means (under our mappings): +// Nothing <: A forSome { type A >: String <: Any } + +// Now to ask the compiler: + + implicitly[Nothing <:< (A forSome { type A >: String <: Any })] + + +// Let's try another: +// +// Proposition: Int :< (M forSome { type M >: String <: Any }) +// +// Bindings: +// T := Int +// U := M +// X1 := M +// L1 := String +// H1 := Any +// +// We need: +// +// Int <: V1 +// String <: V1 +// V1 <: Any +// +// Which simplify to: +// +// V1 >: lub(Int, String) <: Any +// +// V1 >: Any <: Any +// +// We have demonstrated consistency! We can say that: +// T :< (U forSome { type U >: L1 <: H1 }) +// Under our bindings, this is: +// Int :< (M forSome { type M >: String <: Any }) + + implicitly[Int <:< (M forSome { type M >: String <: Any })] + + + +// Now, let's do a more complicated one: +// +// Proposition: (Nothing, List[String]) <: ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] }) +// +// Bindings: +// T := (Nothing, List[String]) +// U := (A, B) +// X1 := A +// X2 := B +// L1 := String +// H1 := AnyRef +// L2 := Null +// H2 := List[A] +// +// We need: +// +// (Nothing, List[String]) <: (V1, V2) +// String <: V1 +// V1 <: AnyRef +// Null <: V2 +// V2 <: List[V1] +// +// Of course, we can split the first line to make: +// +// Nothing <: V1 +// List[String]) <: V2 +// String <: V1 +// V1 <: AnyRef +// Null <: V2 +// V2 <: List[V1] +// +// Which reorder to: +// +// Nothing <: V1 +// String <: V1 +// V1 <: AnyRef +// List[String]) <: V2 +// Null <: V2 +// V2 <: List[V1] +// +// Which simplify to: +// +// String <: V1 +// V1 <: AnyRef +// List[String]) <: V2 +// V2 <: List[V1] +// +// String <: V1 +// V1 <: AnyRef +// String <: V1 +// +// V1 >: String <: AnyRef +// +// Consistency demonstrated! We can say that: +// T <: U forSome {type X1 :> L1 <: H1; type X2 :> L2 <: H2} +// meaning: +// (Nothing, List[String]) <: ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] }) + + implicitly[ + (Nothing, List[String]) <:< ((A, B) forSome { type A >: String <: AnyRef; type B >: Null <: List[A] }) + ] + + + +// Now let's try one that isn't true: +// +// Proposition: Int :< (M forSome { type M >: Nothing <: String }) +// +// Bindings: +// T := Int +// U := M +// X1 := M +// L1 := Nothing +// H1 := String +// +// We need: +// +// Int <: V1 +// Nothing <: V1 +// V1 <: String +// +// V1 >: Int <: String +// +// Alas! These are inconsistent! There is no supertype of Int that is a +// subtype of String! Our substitution rule does not allow us to claim that our +// proposition is true. +// + + implicitly[Int <:< (M forSome { type M >: Nothing <: String })] // fails +// The preceeding line causes the compiler to generate an error message. + + + +// Let's look at one final example, courtesy of paulp. +// Proposition: String :< X forSome { type X >: Nothing <: String } +// +// Bindings: +// T := String +// U := X +// X1 := X +// L1 := Nothing +// H1 := String +// +// We need: +// +// String <: V1 +// Nothing <: V1 +// V1 <: String +// +// Which simplify to: +// +// String <: V1 +// V1 <: String +// +// V1 >: String <: String +// +// So, we can say: +// T <: U forSome { type X1 >: L1 <: H1 } +// which means: +// String :< X forSome { type X >: Nothing <: String } + + implicitly[String <:< (X forSome { type X >: Nothing <: String })] + +} -- cgit v1.2.3