> While normaly forall plays a role of the "universal quantifier", it can also play a role of the "existential quantifier" (depends on the situation). > What i

> While normaly forall plays a role of the "universal quantifier", it can also play a role of the "existential quantifier" (depends on the situation). > What is interesting is that in this case, forall plays the role of an existential quantifier (therefore the name of extension, ExistentialQuantification), unlike the role of universal quantifier it normally plays. This isn't really true. While you can indeed use "forall" to write something that's equivalent to an existentially quantified statement <https://en.wikipedia.org/wiki/Prenex_normal_form#Conversion_to_prenex_form https://en.wikipedia.org/wiki/Prenex_normal_form#Conversion_...> (and that is how you use existential types in Haskell), that doesn't mean it's playing that role. That'd be like saying that the word "all" in "not all X are Y" is playing the role of "some", since that statement means the same thing as "some X are not Y".