One of the things I have a hard time truly internalising is the difference between existentials and universals (written sometimes as exists and forall). They have a very strange relationship and its hard to maintain the intuitions about what each of them mean, other than in the most obvious of interpretations. I remember Prof Mike Dunn, who is a renovned logician and was the Dean of the School of Informatics, in his classes on Galois logics would say that he keeps mixing them up because they are duals of each other.

One area where these crop up and innevitably confuses me is in type theory, especially when looking at the types of continuations. Its at times like this Prof Sabry would saying something mystical sounding, in true sufi style, which will leave me with a little flashlight to use in the darkness.

So some intuitions. What is a universal? Consider the function "head" that takes a list and returns the first element of the list. The function does not concern itself with the types of the quantities in the list, it only cares about the list itself.

So "head" has the type: forall x. List x -> x

(Functions like this may show up when programming with generics (or templates) in some languages. You are free to make these connections, I wont make them here.)

What is the type of head saying? It says that it doesnt care about the underlying type of elements in the list. It only cares about the fact that these elements are in a list. So when head is invoked with a list of integers, "List Int", it returns an integer, "Int". When called with "List String", it returns "String". When called with "List (List Int)" it returns "List String". You get the idea. The "idea" should have two parts (1) "head" is concerned about the fact that it gets an abstract List. (2) There is nothing, no code, inside "head" that depends in anyway on the type of the contents of the list. If head is called with a "List Int" it cannot return an integer that it had hidden off in a variable. It can produce an "Int" only by looking into the List. Why? Beacuse head did not know that its argument would be a list of "Int".

In other words the "forall" says that "head" is truly independant of the type "x". It can manipulate the List, but it can't manipulate the "x". Its is "pure" with respect to "x". The "x" in the List is abstracted away from it. Having a function that is forall quantified is different from having several functions, one for each datatype that you have in your system, because of two reasons (1) There can be an infinite number of data types, which means you will have to have an infinite number of such functions (2) Each such function is for a specific type, "List Int -> Int", and hence knows that it need not ever look into the List but can return any Int to you to satisfy its type; in other words each such function is not "pure" wrt the type of the elements of the list.