Tutorial: `Forall` in Haskell – Wasp

I always write existential quantification

  data Showable = forall a. Show a => Showable a

with GADT syntax because it can be confusing for people to infer the type of `Showable' from the above definition when you can write it out

  data Showable where
    Showable :: Show a => a -> Showable

josephcsible is right. `forall.' in that context doesn't play a different role. Rather a variable bound by `forall.' is logically the same as existential quantification if it does not appear in the return type which `a' doesn't:

  Showable :: forall a. Show a => a -> Showable

We will get a proper existential quantifier soon

* https://github.com/ghc-proposals/ghc-proposals/pull/473 * https://richarde.dev/papers/2021/exists/exists.pdf

and then

  length :: forall a. [a] -> Int

can be replaced with

  length :: (exists a. [a]) -> Int

and `Showable' will be isomorphic to the "packed constraint" `exists a. Show a ∧ a', explained in the paper. This is a tupled constraint, not a function: `(Dict (Show a), a)'

> 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_...> (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".