[Haskell-cafe] Type system madness

[Daniil Elovkov]

2007/7/10, Andrew Coppin <andrewcoppin at btinternet.com>:
>
> I stand in awe of people who actually understand what "universal" and
> "existential" actually mean... To me, these are just very big words that
> sound impressive.
>

The following is only my own understanding, please correct me if it's
totally wrong!
(and sorry for confusion if it is)

Another thing that might help is looking at non-functional values:

forall a. [a] is the _intersection_ of types [a] where 'a' runs over
all possible types.
That is, the only non-bottom value of forall a. [a] is the empty list [].
So, [4,5] doesn't belong to this type, nor does ['H','e','y'].

exists a. [a] constains [4,5] and "Hey" and []. So, it's tempting to
say, that it is the sum of types [a] where 'a' runs over all possible
types, but I may be lacking theoretic background here...

However, in Haskell both of those are designated by the forall word,
because as a consumer you treat them in the same way. That is, you
can't (safely) make any assumptions about 'a'. In case of forall it
simply doesn't make sense, in case of exists Haskell doesn't give you
the means to know what 'a' was really used when the value was created.

So, if you have types forall a. Class a => [a] and exists a. Class a
=> [a], in both cases all that you can do with the value is

1) what you can do with lists
2) what you can do with instances of Class (that's for elements of the list)