Fw: Modification of State Transformer

Shawn P. Garbett Shawn@Garbett.org
Mon, 12 Aug 2002 14:24:10 -0500


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

On Monday 12 August 2002 02:08 pm, Scott J. wrote:
> ----- Original Message -----
> From: "Scott J." <jscott@planetinternet.be>
> > What I meant was discussion about the state transformer ST s a itself.
> > And how it works. What does mean the second inner forall loop and so on.
> > I can't find explanations of this in the Haskell library.

Oh!

If you look in the paper that's mentioned: _Lazy_Functional_State_Threads_, 
by John Launchbury and Simon Jones, 1994, there's a big section on this.

To quote:

Section 2.4 Encapsulaion

"So far we have been able to combine state transformers to make larger state 
transformers, but how can we make a state transformer part of a larger 
program which does not manipulate state at all? What we need is a function, 
runST, with a type something like the following:
	runST :: ST s a -> a"

"The idea is that runST takes a state transformer as its argument, conjures up
an initial empty state, applies the state transformer to it, and returns the
result while discarding the final state."

... Discussion of usage implications, and how this initial guess at type 
creates all kinds of potential usage problems ...

"To put it another way, the argument of runST should no make any assumptions 
about what has already been allocated in the initial state, That is, runST 
should work regardless of what initial state it is given. So the type of 
runST should be:
	runST :: forall a . (forall s.ST s a) -> a
This is not a Hindley-Milner type, because the quantifiers are not all at the 
top level; it is an example of rank-2 polymorphism (McCracken [1984]).

Section 5.2 Types

"Most of the type rules are the usual Hindley-Milner rules. The most 
interesting addition is the typing judgement for runST. Treating it as a 
language construct avoids the need to go beyond Hindley-Milner types. So 
rather than actually give runST the type
	runST :: forall a . (forall s.ST s a) -> a
as suggested in the introduction, we ensure that its typing judgment has the 
same effect."


- -- 
You're in a maze of twisty little statements, all alike.
Public Key available from http://www.garbett.org/public-key
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.0.7 (GNU/Linux)

iD8DBQE9WAthDtpPjAQxZ6ARAgsqAJ9i+oIdWHvQB80xmEhugQTklOtpvQCdFbM5
ol6XOKjp7FGdM3oetPUTw+E=
=+exg
-----END PGP SIGNATURE-----