# Question aboutthe use of an inner forall

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

```This is a multi-part message in MIME format.

------=_NextPart_000_0009_01C2473F.0CFB6930
Content-Type: text/plain;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

Ok, a and s are type variables. It may be common usage for computer =
people but for someone with a math background it is difficult to call =
forall a a type . In logic one expects a statement in the scope of =
forall a like this

(forall a) statement. The statement may or may not depend on a.

So let's come backe to runST.

runST ::( forall s) (ST s a )-> a

So I insist what is the statement ST s a ?

Scott

----- Original Message -----=20
From: "Ashley Yakeley" <ashley@semantic.org>
To: "Scott J." <jscott@planetinternet.be>
Sent: Monday, August 19, 2002 4:26 AM
Subject: Re: Question aboutthe use of an inner forall

> At 2002-08-18 18:19, Scott J. wrote:
>=20
> >A question: s is not a type variable as a isn't it?
>=20
> Both are quantified type variables. But only one of those quantifiers =
can=20
> be placed at the top level of the expression.
>=20
>    runST :: forall a. ((forall s. ST s a) -> a)
>=20
> > I mean a can be of type Integer while s cannot.
>=20
> Well yes, you can specialise "forall a" to Integer. So runST can be=20
> specialised to this type:
>=20
>    runST ::[special] (forall s. ST s Integer) -> Integer
>=20
> ...whereas you cannot specialise "s" in the same way. Think of it in=20
> terms of logic, if for all a: f(a), then by simple specialisation=20
> f(Integer).
>=20
> --=20
> Ashley Yakeley, Seattle WA
>=20
>=20

------=_NextPart_000_0009_01C2473F.0CFB6930
Content-Type: text/html;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<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>
<BODY>
<DIV><FONT face=3DArial size=3D2>Ok, a and s are type variables. It may =
be common=20
usage for computer people but for someone with a math background it is =
difficult=20
to call <STRONG>forall a </STRONG>a type . In logic one expects a =
statement in=20
the scope of <STRONG>forall a </STRONG>like this</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2><STRONG>(forall a) <FONT=20
color=3D#ff0000>statement</FONT>.</STRONG> The statement may or may not =
depend on=20
a.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>So let's come backe to =
runST.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>runST ::( forall s) <FONT =
color=3D#ff0000><FONT=20
color=3D#000000>(</FONT><STRONG>ST s a</STRONG> </FONT><FONT =
color=3D#000000>)-&gt;=20
a</FONT></FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT>&nbsp;</DIV>
<DIV><FONT face=3DArial size=3D2>So I insist what is the =
<STRONG>statement</STRONG>=20
<FONT color=3D#ff0000><STRONG>ST s a</STRONG> </FONT><FONT=20
color=3D#000000>?</FONT></FONT></DIV>
<DIV><STRONG><FONT face=3DArial color=3D#ff0000 =
size=3D2></FONT></STRONG>&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: "Ashley Yakeley" &lt;</FONT><A=20
href=3D"mailto:ashley@semantic.org"><FONT face=3DArial=20
size=3D2>ashley@semantic.org</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=20
size=3D2>&gt;</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Cc: "Haskell Cafe List" &lt;</FONT><A=20
size=3D2>&gt;</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Sent: Monday, August 19, 2002 4:26 =
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; At 2002-08-18 18:19, Scott J. wrote:<BR>&gt; <BR>&gt; =
&gt;A=20
question: s is not a type variable as a isn't it?<BR>&gt; <BR>&gt; Both =
are=20
quantified type variables. But only one of those quantifiers can =
<BR>&gt; be=20
placed at the top level of the expression.<BR>&gt; <BR>&gt; &nbsp;&nbsp; =
runST=20
:: forall a. ((forall s. ST s a) -&gt; a)<BR>&gt; <BR>&gt; &gt; I mean a =
can be=20
of type Integer while s cannot.<BR>&gt; <BR>&gt; Well yes, you can =
specialise=20
"forall a" to Integer. So runST can be <BR>&gt; specialised to this=20
type:<BR>&gt; <BR>&gt; &nbsp;&nbsp; runST ::[special] (forall s. ST s =
Integer)=20
-&gt; Integer<BR>&gt; <BR>&gt; ...whereas you cannot specialise "s" in =
the same=20
way. Think of it in <BR>&gt; terms of logic, if for all a: f(a), then by =
simple=20
specialisation <BR>&gt; f(Integer).<BR>&gt; <BR>&gt; -- <BR>&gt; Ashley =
Yakeley,=20
Seattle WA<BR>&gt; <BR>&gt; </FONT></BODY></HTML>

------=_NextPart_000_0009_01C2473F.0CFB6930--

```