Universal Quantification, Bound and Existential Quantification

Universal quantification is usually not very useful. Inside the body of a universal quantified function, what you know about the argument is very general, because the argument can be *any* type. Suppose you're writing a function with type *->Int, what do you think the function can do? The only implementation I can think of is a constant function:

(pseudo codes)

  f1 :: [forall a] a -> Int
  f1 x = 1

In contrast, existential quantified functions are very useful, because there're always *some* types can do certain things. Use the same example:

  f2 :: [exist a] a -> Int
  f2 x = length x

I can do nearly anything inside f2, because there's always some x will satify the operations applied on them.

You should notice that only functions or Bottom can have universal quantified type.

Bound helps universal quantification a lot. When you give a bound to universal quantification, you give it extra informations.