[Haskell-cafe] Type system madness

[Jonathan Cast]

On Tuesday 10 July 2007, Andrew Coppin wrote:
> 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??

Are you serious?  Unicode has been a (more-or-less) working reality on Linux 
for several years now. . .

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

Exactly.

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

Jonathan Cast
http://sourceforge.net/projects/fid-core
http://sourceforge.net/projects/fid-emacs