On Mon, Jul 09, 2007 at 09:57:14PM +0100, Andrew Coppin wrote:
Stefan O'Rear wrote:
id has type :: ∀α. α → α
toUpper (can) have type :: ∃α. α → α
So... you're saying that id:: x -> x works for *every* possible choice of x, but toUpper :: x -> x works for *one* possible choice of x?
[JonCast answered this one]
(BTW... How in the hell do you get symbols like that in plain ASCII??)
You can't, but the most commonly used replacement for ASCII (Unicode-UTF8) supports them just fine. As for actually *entering* the characters, I have a file with the code numbers of the characters I use most often: 039B Λ big lambda 03BB λ little lambda 2203 ∃ existensial quant 2200 ∀ universal quant 2192 → right arrow 03B2 β beta 22A5 ⊥ bottom 00F6 ö o-umlaut (alpha isn't on there, but I guessed (correctly) it would be right before beta)
If you're at all familiar with mathematics logic, don't hesistate to apply your intuitions about forall and exists - type systems and logics really are the same things.
I have wide interests in diverse areas of science, mathematics and computing, covering everything from cryptology to group theory to data compression - but formal logic is something I've never been able to bend my mind around. :-(
Don't worry - you can understand the material equally well from either direction. Personally I didn't really understand logic until seeing type systems and then the Curry-Howard isomorphism (types are propositions, programs are proofs).
If you have a value of existential type, you can only do things with it that you can do with any type, because you don't know the actual type. Existential types hide information from the users.
If you have a value of universal type, you can do things with it as if it had any matching type of your choice, because it doesn't know and can't care about the actual use type. Universal types hide information from the implementors.
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.
So, are you saying that if x is existential, it must work for any possible x, but if x is universal, I can choose what x is?
[JonCast answered this one]
In Haskell 98, existential quantification is not supported at all, and universal quantification is not first class - values can have universal types if and only if they are bound by let. You cannot pass universally typed values to functions.
Erm...
Consider the ST monad, which lets you use update-in-place, but is escapable (unlike IO). ST actions have the form: ST s α Meaning that they return a value of type α, and execute in "thread" s. All reference types are tagged with the thread, so that actions can only affect references in their own "thread". Now, the type of the function used to escape ST is: runST :: ∀ α. (∀ s. ST s α) → α The action you pass must be universal in s, so inside your action you don't know what thread, thus you cannot access any other threads, thus runST is pure. This is very useful, since it allows you to implement externally pure things like in-place quicksort, and present them as pure functions ∀ e. Ord e ⇒ Array e → Array e; without using any unsafe functions. But that type of runST is illegal in Haskell-98, because it needs a universal quantifier *inside* the function-arrow! In the jargon, that type has rank 2; haskell 98 types may have rank at most 1. Stefan