[Haskell-cafe] Type system madness

Andrew Coppin andrewcoppin at btinternet.com
Tue Jul 10 15:02:35 EDT 2007


Stefan O'Rear wrote:
> On Mon, Jul 09, 2007 at 09:57:14PM +0100, Andrew Coppin wrote:
>   
>> (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.

Wait... I thought Unicode was still an experimental prototype? Since 
when does it work in the real world??

> 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".
>   

...so *that* is what that thing does...! (I thought it did something 
quite different.)

> 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.
>   

...so the 's' doesn't really "exist", it's just random hackery of the 
type system to implement uniqueness?

> 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.
>   

...kinda wishing I hadn't asked... o_O



More information about the Haskell-Cafe mailing list