Fw: Question aboutthe use of an inner forall
Scott J.
jscott@planetinternet.be
Mon, 19 Aug 2002 05:46:29 +0200
This is a multi-part message in MIME format.
------=_NextPart_000_0028_01C24743.C432A6F0
Content-Type: text/plain;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Again a typo. Please read something like MutVar s Bool. Sorry
Scott
----- Original Message -----=20
From: Scott J.=20
To: Jay Cox=20
Cc: haskell-cafe@haskell.org=20
Sent: Monday, August 19, 2002 5:41 AM
Subject: Re: Question aboutthe use of an inner forall
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_0028_01C24743.C432A6F0
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 bgColor=3D#ffffff>
<DIV><FONT face=3DArial size=3D2>Again a typo. Please read something =
like MutVar s=20
Bool. Sorry</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>Scott</FONT></DIV>
<DIV> </DIV>
<DIV style=3D"FONT: 10pt arial">----- Original Message -----=20
<DIV style=3D"BACKGROUND: #e4e4e4; font-color: black"><B>From:</B> <A=20
title=3Djscott@planetinternet.be =
href=3D"mailto:jscott@planetinternet.be">Scott=20
J.</A> </DIV>
<DIV><B>To:</B> <A title=3Dsqrtofone@yahoo.com=20
href=3D"mailto:sqrtofone@yahoo.com">Jay Cox</A> </DIV>
<DIV><B>Cc:</B> <A title=3Dhaskell-cafe@haskell.org=20
href=3D"mailto:haskell-cafe@haskell.org">haskell-cafe@haskell.org</A> =
</DIV>
<DIV><B>Sent:</B> Monday, August 19, 2002 5:41 AM</DIV>
<DIV><B>Subject:</B> Re: Question aboutthe use of an inner =
forall</DIV></DIV>
<DIV><BR></DIV>
<DIV><FONT face=3DArial size=3D2>Well I don't feel alone =
anymore.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>Here follows how I think runST :: =
(forall s. ST s=20
a) -> a works:</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>if a is represented by =
e.g.=20
<STRONG>MutVar s a</STRONG> . Then the compiler complains because it did =
find 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> </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> </DIV>
<DIV><FONT face=3DArial size=3D2>Scott</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>----- Original Message ----- </FONT>
<DIV><FONT face=3DArial size=3D2>From: "Jay Cox" <</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>></FONT></DIV>
<DIV><FONT face=3DArial size=3D2>To: "Scott J." <</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>>; "Haskell=20
Cafe List" <</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>></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>> <BR>> ----- Original Message -----<BR>> From: =
"Ashley Yakeley"=20
<</FONT><A href=3D"mailto:ashley@semantic.org"><FONT face=3DArial=20
size=3D2>ashley@semantic.org</FONT></A><FONT face=3DArial =
size=3D2>><BR>> To:=20
"Scott J." <</FONT><A href=3D"mailto:jscott@planetinternet.be"><FONT =
face=3DArial=20
size=3D2>jscott@planetinternet.be</FONT></A><FONT face=3DArial =
size=3D2>>; "Haskell=20
Cafe List"<BR>> <</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>><BR>> Sent: Friday, August 16, 2002 11:15 PM<BR>> =
Subject: Re:=20
Question aboutthe use of an inner forall<BR>> <BR>> <BR>> > =
At=20
2002-08-16 20:57, Scott J. wrote:<BR>> ><BR>> > >However =
what for=20
heaven's sake should I think of<BR>> > ><BR>> > >runST =
::=20
forall a ( forall s ST s a) -> a ?<BR>> ><BR>> =
> =20
runST :: forall a. ((forall s. ST s a) -> a)<BR>> ><BR>> =
> "For=20
all a, if (for all s, (ST s a)) then a."<BR>> ><BR>> > You =
may apply=20
runST to anything with a type of the form (forall s. ST s<BR>> > =
a), for=20
any 'a'.<BR>> <BR>> I'm very fuzzy to the details of type theory =
in=20
general so please forgive<BR>> any errors.<BR>> <BR>> I noted =
the same=20
question as Scott's when I first learned about ST threads.<BR>> =
<BR>> When=20
you have a rank-2 polymorphic function, like<BR>> <BR>> =
runST::forall a .=20
( forall s . ST s a) -> a<BR>> <BR>> the type means the =
function takes=20
an argument ***at least as polymorphic***<BR>> as<BR>> (forall s . =
ST s=20
(some type a independent of s)). If (runST stthread ) has<BR>> =
type=20
String, then stthread must at least have type ST s String.<BR>> =
<BR>> Why=20
do you need this apparent mumbo jumbo about Rank-2 polymorphism? =20
It<BR>> insures your ST threads are threadsafe (or so I have been led =
to=20
believe).<BR>> You will not be able to throw a mutable reference =
outside of=20
the thread.<BR>> <BR>> take this long interaction from ghci =
(the=20
ST> is the prompt, and what<BR>> follows<BR>> on the same line =
is the=20
code entered. For instance :type gives the type of<BR>> the =
following=20
code. I have separated ghci input/ouput from comments by<BR>> =
placing #=20
in front of the IO).<BR>> <BR>> #ST> :type newSTRef=20
(3::Prelude.Int)<BR>> #forall s. ST s (STRef s PrelBase.Int)<BR>> =
<BR>>=20
The type variable a is replaced by, or a has the value of, (STRef =
s<BR>>=20
PrelBase.Int). but this depends on s.<BR>> <BR>> #ST> :type=20
readSTRef<BR>> #forall s a. STRef s a -> ST s a<BR>> #ST> =
:type (do=20
x<-newSTRef (3::Prelude.Int);readSTRef x)<BR>> #forall s. ST s=20
PrelBase.Int<BR>> <BR>> a here is replaced by PrelBase.Int. the =
code in=20
the do statement is runnable<BR>> with runST<BR>> <BR>> #ST> =
runST=20
(newSTRef (3::Prelude.Int))<BR>> #<BR>> #Ambiguous type =
variable(s) `a' in=20
the constraint `PrelShow.Show a'<BR>> #arising from use of =
`PrelIO.print' at=20
<No locn><BR>> #In a 'do' expression pattern binding: =
PrelIO.print=20
it<BR>> #<BR>> #<interactive>:1:<BR>> # =
Inferred type is less polymorphic than expected<BR>>=20
# Quantified type variable `s' =
escapes<BR>> # It is =
reachable from=20
the type variable(s) `a'<BR>>=20
# which is free in =
the=20
signature<BR>> # Signature =
type: =20
forall s. ST s a<BR>> # Type to generalise: ST s1 =
(STRef s1=20
PrelBase.Int)<BR>> # When checking an expression =
type=20
signature<BR>> # In the first argument of `runST',=20
namely<BR>> # `(newSTRef (3 =
::=20
PrelBase.Int))'<BR>> # In the definition of `it': =
runST=20
(newSTRef (3 :: PrelBase.Int))<BR>> <BR>> above is a demonstration =
of how=20
the type checking prevents<BR>> using/reading/modifying references =
outside of=20
the ST world.<BR>> <BR>> I realize this is a bit of an incomplete=20
explanation: Some questions I<BR>> would like to answer to help =
your=20
comprehension but cannot due to my<BR>> ignorance are:<BR>> =
<BR>> 1.=20
how do you measure the polymorphic nature of a type so that you =
can=20
say<BR>> it is "at least as polymorphic"? I have a fuzzy idea and =
some=20
examples (Num<BR>> a =3D> a vs. forall a . a vs. forall a . =
[a],=20
etc.) but I haven't yet found<BR>> out for myself a precise=20
definition.<BR>> 2. what does it mean that type variable "escapes", =
and why=20
is it bad? A<BR>> reasonable answer isn't popping into my head =
right=20
now. Something about how<BR>> the type of a program should be =
fully=20
resolved pops into my head but nothing<BR>> cohesive.<BR>> =
<BR>> Maybe=20
that helps.<BR>> <BR>> Jay Cox<BR>> <BR>> <BR>>=20
</FONT></BODY></HTML>
------=_NextPart_000_0028_01C24743.C432A6F0--