Question aboutthe use of an inner forall

Scott J. jscott@planetinternet.be
Mon, 19 Aug 2002 05:41:31 +0200


This is a multi-part message in MIME format.

------=_NextPart_000_001C_01C24743.11FDECB0
Content-Type: text/plain;
	charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

Well I don't feel alone anymore.

Here follows how I think runST :: (forall s. ST s a) -> a works:

if  a is represented  by e.g. MutVar s a . Then the compiler complains =
because it did find  an s in the "data" represented by a. This s must =
first be eliminated by some other combinators(?) .=20

I agree that something must be written for the argument of runST to warn =
programmers about the possible "representations" of a. But I still have =
problems that one has chosen forall.

Scott


----- Original Message -----=20
From: "Jay Cox" <sqrtofone@yahoo.com>
To: "Scott J." <jscott@planetinternet.be>; "Haskell Cafe List" =
<haskell-cafe@haskell.org>
Sent: Monday, August 19, 2002 5:19 AM
Subject: Re: Question aboutthe use of an inner forall


>=20
> ----- Original Message -----
> From: "Ashley Yakeley" <ashley@semantic.org>
> To: "Scott J." <jscott@planetinternet.be>; "Haskell Cafe List"
> <haskell-cafe@haskell.org>
> Sent: Friday, August 16, 2002 11:15 PM
> Subject: Re: Question aboutthe use of an inner forall
>=20
>=20
> > At 2002-08-16 20:57, Scott J. wrote:
> >
> > >However what for heaven's sake should I think of
> > >
> > >runST :: forall a ( forall s ST s a) -> a ?
> >
> >   runST :: forall a. ((forall s. ST s a) -> a)
> >
> > "For all a, if (for all s, (ST s a)) then a."
> >
> > You may apply runST to anything with a type of the form (forall s. =
ST s
> > a), for any 'a'.
>=20
> I'm very fuzzy to the details of type theory in general so please =
forgive
> any errors.
>=20
> I noted the same question as Scott's when I first learned about ST =
threads.
>=20
> When you have a rank-2 polymorphic function, like
>=20
> runST::forall a . ( forall s . ST s a) -> a
>=20
> the type means the function takes an argument ***at least as =
polymorphic***
> as
> (forall s . ST s (some type a independent of s)).  If (runST stthread =
) has
> type String, then stthread must at least have type ST s String.
>=20
> Why do you need this apparent mumbo jumbo about Rank-2 polymorphism?  =
It
> insures your ST threads are threadsafe (or so I have been led to =
believe).
> You will not be able to throw a mutable reference outside of the =
thread.
>=20
> take this long interaction from  ghci (the ST> is the prompt, and what
> follows
> on the same line is the code entered.  For instance :type gives the =
type of
> the following code.  I have separated ghci input/ouput from comments =
by
> placing # in front of the IO).
>=20
> #ST> :type newSTRef (3::Prelude.Int)
> #forall s. ST s (STRef s PrelBase.Int)
>=20
> The type variable a is replaced by, or a has the value of, (STRef s
> PrelBase.Int). but this depends on s.
>=20
> #ST> :type readSTRef
> #forall s a. STRef s a -> ST s a
> #ST> :type (do x<-newSTRef (3::Prelude.Int);readSTRef x)
> #forall s. ST s PrelBase.Int
>=20
> a here is replaced by PrelBase.Int. the code in the do statement is =
runnable
> with runST
>=20
> #ST> runST (newSTRef (3::Prelude.Int))
> #
> #Ambiguous type variable(s) `a' in the constraint `PrelShow.Show a'
> #arising from use of `PrelIO.print' at <No locn>
> #In a 'do' expression pattern binding: PrelIO.print it
> #
> #<interactive>:1:
> #    Inferred type is less polymorphic than expected
> #        Quantified type variable `s' escapes
> #        It is reachable from the type variable(s) `a'
> #          which is free in the signature
> #    Signature type:     forall s. ST s a
> #    Type to generalise: ST s1 (STRef s1 PrelBase.Int)
> #    When checking an expression type signature
> #    In the first argument of `runST', namely
> #        `(newSTRef (3 :: PrelBase.Int))'
> #    In the definition of `it': runST (newSTRef (3 :: PrelBase.Int))
>=20
> above is a demonstration of how the type checking prevents
> using/reading/modifying references outside of the ST world.
>=20
> I realize this is a bit of an incomplete explanation:  Some questions =
I
> would like to answer to help your comprehension but cannot due to my
> ignorance are:
>=20
> 1. how do you measure the polymorphic nature of a type  so that you =
can say
> it is "at least as polymorphic"? I have a fuzzy idea and some examples =
(Num
> a =3D> a vs. forall a . a vs.  forall a . [a], etc.)  but I haven't =
yet found
> out for myself a precise definition.
> 2. what does it mean that type variable "escapes", and why is it bad?  =
A
> reasonable answer isn't popping into my head right now.  Something =
about how
> the type of a program should be fully resolved pops into my head but =
nothing
> cohesive.
>=20
> Maybe that helps.
>=20
> Jay Cox
>=20
>=20
>=20

------=_NextPart_000_001C_01C24743.11FDECB0
Content-Type: text/html;
	charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META http-equiv=3DContent-Type content=3D"text/html; =
charset=3Diso-8859-1">
<META content=3D"MSHTML 6.00.2716.2200" name=3DGENERATOR>
<STYLE></STYLE>
</HEAD>
<BODY>
<DIV><FONT face=3DArial size=3D2>Well I don't feel alone =
anymore.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>Here follows how I think runST :: =
(forall s. ST s=20
a) -&gt; a works:</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>if&nbsp; a is represented&nbsp;&nbsp;by =
e.g.=20
<STRONG>MutVar s a</STRONG> . Then the compiler complains because it did =

find&nbsp; an <STRONG>s</STRONG> in the "data" represented by a. This=20
<STRONG>s</STRONG> must first be eliminated by some other combinators(?) =
.=20
</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>I agree that something must be written =
for the=20
argument of runST to warn programmers about the possible =
"representations" of a.=20
But I still have problems that one has chosen=20
<STRONG>forall.</STRONG></FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>Scott</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>----- Original Message ----- </FONT>
<DIV><FONT face=3DArial size=3D2>From: "Jay Cox" &lt;</FONT><A=20
href=3D"mailto:sqrtofone@yahoo.com"><FONT face=3DArial=20
size=3D2>sqrtofone@yahoo.com</FONT></A><FONT face=3DArial =
size=3D2>&gt;</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>To: "Scott J." &lt;</FONT><A=20
href=3D"mailto:jscott@planetinternet.be"><FONT face=3DArial=20
size=3D2>jscott@planetinternet.be</FONT></A><FONT face=3DArial =
size=3D2>&gt;; "Haskell=20
Cafe List" &lt;</FONT><A href=3D"mailto:haskell-cafe@haskell.org"><FONT =
face=3DArial=20
size=3D2>haskell-cafe@haskell.org</FONT></A><FONT face=3DArial=20
size=3D2>&gt;</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Sent: Monday, August 19, 2002 5:19 =
AM</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Subject: Re: Question aboutthe use of =
an inner=20
forall</FONT></DIV></DIV>
<DIV><FONT face=3DArial><BR><FONT size=3D2></FONT></FONT></DIV><FONT =
face=3DArial=20
size=3D2>&gt; <BR>&gt; ----- Original Message -----<BR>&gt; From: =
"Ashley Yakeley"=20
&lt;</FONT><A href=3D"mailto:ashley@semantic.org"><FONT face=3DArial=20
size=3D2>ashley@semantic.org</FONT></A><FONT face=3DArial =
size=3D2>&gt;<BR>&gt; To:=20
"Scott J." &lt;</FONT><A href=3D"mailto:jscott@planetinternet.be"><FONT =
face=3DArial=20
size=3D2>jscott@planetinternet.be</FONT></A><FONT face=3DArial =
size=3D2>&gt;; "Haskell=20
Cafe List"<BR>&gt; &lt;</FONT><A =
href=3D"mailto:haskell-cafe@haskell.org"><FONT=20
face=3DArial size=3D2>haskell-cafe@haskell.org</FONT></A><FONT =
face=3DArial=20
size=3D2>&gt;<BR>&gt; Sent: Friday, August 16, 2002 11:15 PM<BR>&gt; =
Subject: Re:=20
Question aboutthe use of an inner forall<BR>&gt; <BR>&gt; <BR>&gt; &gt; =
At=20
2002-08-16 20:57, Scott J. wrote:<BR>&gt; &gt;<BR>&gt; &gt; &gt;However =
what for=20
heaven's sake should I think of<BR>&gt; &gt; &gt;<BR>&gt; &gt; &gt;runST =
::=20
forall a ( forall s ST s a) -&gt; a ?<BR>&gt; &gt;<BR>&gt; =
&gt;&nbsp;&nbsp;=20
runST :: forall a. ((forall s. ST s a) -&gt; a)<BR>&gt; &gt;<BR>&gt; =
&gt; "For=20
all a, if (for all s, (ST s a)) then a."<BR>&gt; &gt;<BR>&gt; &gt; You =
may apply=20
runST to anything with a type of the form (forall s. ST s<BR>&gt; &gt; =
a), for=20
any 'a'.<BR>&gt; <BR>&gt; I'm very fuzzy to the details of type theory =
in=20
general so please forgive<BR>&gt; any errors.<BR>&gt; <BR>&gt; I noted =
the same=20
question as Scott's when I first learned about ST threads.<BR>&gt; =
<BR>&gt; When=20
you have a rank-2 polymorphic function, like<BR>&gt; <BR>&gt; =
runST::forall a .=20
( forall s . ST s a) -&gt; a<BR>&gt; <BR>&gt; the type means the =
function takes=20
an argument ***at least as polymorphic***<BR>&gt; as<BR>&gt; (forall s . =
ST s=20
(some type a independent of s)).&nbsp; If (runST stthread ) has<BR>&gt; =
type=20
String, then stthread must at least have type ST s String.<BR>&gt; =
<BR>&gt; Why=20
do you need this apparent mumbo jumbo about Rank-2 polymorphism?&nbsp;=20
It<BR>&gt; insures your ST threads are threadsafe (or so I have been led =
to=20
believe).<BR>&gt; You will not be able to throw a mutable reference =
outside of=20
the thread.<BR>&gt; <BR>&gt; take this long interaction from&nbsp; ghci =
(the=20
ST&gt; is the prompt, and what<BR>&gt; follows<BR>&gt; on the same line =
is the=20
code entered.&nbsp; For instance :type gives the type of<BR>&gt; the =
following=20
code.&nbsp; I have separated ghci input/ouput from comments by<BR>&gt; =
placing #=20
in front of the IO).<BR>&gt; <BR>&gt; #ST&gt; :type newSTRef=20
(3::Prelude.Int)<BR>&gt; #forall s. ST s (STRef s PrelBase.Int)<BR>&gt; =
<BR>&gt;=20
The type variable a is replaced by, or a has the value of, (STRef =
s<BR>&gt;=20
PrelBase.Int). but this depends on s.<BR>&gt; <BR>&gt; #ST&gt; :type=20
readSTRef<BR>&gt; #forall s a. STRef s a -&gt; ST s a<BR>&gt; #ST&gt; =
:type (do=20
x&lt;-newSTRef (3::Prelude.Int);readSTRef x)<BR>&gt; #forall s. ST s=20
PrelBase.Int<BR>&gt; <BR>&gt; a here is replaced by PrelBase.Int. the =
code in=20
the do statement is runnable<BR>&gt; with runST<BR>&gt; <BR>&gt; #ST&gt; =
runST=20
(newSTRef (3::Prelude.Int))<BR>&gt; #<BR>&gt; #Ambiguous type =
variable(s) `a' in=20
the constraint `PrelShow.Show a'<BR>&gt; #arising from use of =
`PrelIO.print' at=20
&lt;No locn&gt;<BR>&gt; #In a 'do' expression pattern binding: =
PrelIO.print=20
it<BR>&gt; #<BR>&gt; #&lt;interactive&gt;:1:<BR>&gt; #&nbsp;&nbsp;&nbsp; =

Inferred type is less polymorphic than expected<BR>&gt;=20
#&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; Quantified type variable `s' =

escapes<BR>&gt; #&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; It is =
reachable from=20
the type variable(s) `a'<BR>&gt;=20
#&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; which is free in =
the=20
signature<BR>&gt; #&nbsp;&nbsp;&nbsp; Signature =
type:&nbsp;&nbsp;&nbsp;&nbsp;=20
forall s. ST s a<BR>&gt; #&nbsp;&nbsp;&nbsp; Type to generalise: ST s1 =
(STRef s1=20
PrelBase.Int)<BR>&gt; #&nbsp;&nbsp;&nbsp; When checking an expression =
type=20
signature<BR>&gt; #&nbsp;&nbsp;&nbsp; In the first argument of `runST',=20
namely<BR>&gt; #&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; `(newSTRef (3 =
::=20
PrelBase.Int))'<BR>&gt; #&nbsp;&nbsp;&nbsp; In the definition of `it': =
runST=20
(newSTRef (3 :: PrelBase.Int))<BR>&gt; <BR>&gt; above is a demonstration =
of how=20
the type checking prevents<BR>&gt; using/reading/modifying references =
outside of=20
the ST world.<BR>&gt; <BR>&gt; I realize this is a bit of an incomplete=20
explanation:&nbsp; Some questions I<BR>&gt; would like to answer to help =
your=20
comprehension but cannot due to my<BR>&gt; ignorance are:<BR>&gt; =
<BR>&gt; 1.=20
how do you measure the polymorphic nature of a type&nbsp; so that you =
can=20
say<BR>&gt; it is "at least as polymorphic"? I have a fuzzy idea and =
some=20
examples (Num<BR>&gt; a =3D&gt; a vs. forall a . a vs.&nbsp; forall a . =
[a],=20
etc.)&nbsp; but I haven't yet found<BR>&gt; out for myself a precise=20
definition.<BR>&gt; 2. what does it mean that type variable "escapes", =
and why=20
is it bad?&nbsp; A<BR>&gt; reasonable answer isn't popping into my head =
right=20
now.&nbsp; Something about how<BR>&gt; the type of a program should be =
fully=20
resolved pops into my head but nothing<BR>&gt; cohesive.<BR>&gt; =
<BR>&gt; Maybe=20
that helps.<BR>&gt; <BR>&gt; Jay Cox<BR>&gt; <BR>&gt; <BR>&gt;=20
</FONT></BODY></HTML>

------=_NextPart_000_001C_01C24743.11FDECB0--