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 preceding 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 })]
}
