This is Martin Odersky’s answer on the Scala-users mailing list: The original Java wildcard types (as described in the ECOOP paper by Igarashi and Viroli) were indeed just shorthands for existential types. I am told and I have read in the FOOL ’05 paper on Wild FJ that the final version of wildcards has some … Read more
Existential types work in a more elaborate manner than regular types. GHC is (rightly) forbidding you from using theA as a function. But imagine there was no such prohibition. What type would that function have? It would have to be something like this: — Not a real type signature! theA :: ALL -> t — … Read more
Attention: (Update 2016-12-08) The forSome keyword is very likely going away with Scala 2.13 or 2.14, according to Martin Odersky’s talk on the ScalaX 2016. Replace it with path dependent types or with anonymous type attributes (A[_]). This is possible in most cases. If you have an edge case where it is not possible, refactor … Read more
The terms “universal” and “existential” here come from the similarly-named quantifiers in predicate logic. Universal quantification is normally written as ∀, which you can read as “for all”, and means roughly what it sounds like: in a logical statement resembling “∀x. …” whatever is in place of the “…” is true for all possible “x” … Read more
First of all, take a look at the “Curry Howard correspondence” which states that the types in a computer program correspond to formulas in intuitionistic logic. Intuitionistic logic is just like the “regular” logic you learned in school but without the law of the excluded middle or double negation elimination: Not an axiom: P ⇔ … Read more
OK, I figured I should have my take on it, instead of just posting comments. Sorry, this is going to be long, if you want the TL;DR skip to the end. As Randall Schulz said, here _ is a shorthand for an existential type. Namely, class Foo[T <: List[_]] is a shorthand for class Foo[T … Read more
When someone defines a universal type ∀X they’re saying: You can plug in whatever type you want, I don’t need to know anything about the type to do my job, I’ll only refer to it opaquely as X. When someone defines an existential type ∃X they’re saying: I’ll use whatever type I want here; you … Read more