[Haskell-cafe] Type system madness

[Stefan O'Rear]

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20070709/82b1d074/attachment.bin