Question aboutthe use of an inner forall
Scott J.
jscott@planetinternet.be
Sat, 17 Aug 2002 05:57:46 +0200
This is a multi-part message in MIME format.
------=_NextPart_000_0035_01C245B3.02659730
Content-Type: text/plain;
charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Hi,
It goes about the State tansformer monad ST s a. I think how it works =
but as a logician the use of an internal forall is difficult to swallow.
Let's first see a statement in Haskell.
One can type foo :: a -> b as a function We can be not sloppy (but this =
gives unnecessary clutter in the program I think) and type it as:
forall a,b foo :: a -> b
Now this is a statement in logic, it can be true or false.=20
However what for heaven's sake should I think of
runST :: forall a ( forall s ST s a) -> a ?
In logic forall x forall y statement(x.y) is equivalent to: forall y =
forall x statement(x,y).
Why the use of the inner forall in runST?This is not a normal function =
declaration in mathematics. Since Haskell is Hindley-Milner typed and =
can't use an inner forall . Why the use an inner forall. Has imagination =
dried up (sorry, if this seems impolite)?
Thx
Scott
------=_NextPart_000_0035_01C245B3.02659730
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>Hi,</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>It goes about the State tansformer =
monad <STRONG>ST=20
s a</STRONG>. I think how it works but as a logician the use of an =
internal=20
forall is difficult to swallow.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>Let's first see a <STRONG>statement =
</STRONG>in=20
Haskell.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>One can type <STRONG>foo :: a -> =
b</STRONG> as a=20
function We can be not sloppy (but this gives unnecessary clutter in the =
program=20
I think) and type it as:</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2><STRONG>forall</STRONG> a,b foo :: a =
->=20
b</FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Now this is a statement in logic, it =
can be true or=20
false. </FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>However what for heaven's sake should I =
think=20
of</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>runST :: forall a ( forall s ST s a) =
-> a=20
?</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>In logic <STRONG>forall x forall y=20
statement(x.y)</STRONG> is <EM>equivalent</EM> to: <STRONG>forall y =
forall=20
x</STRONG> <STRONG>statement(x,y).</STRONG></FONT></DIV>
<DIV><STRONG><FONT face=3DArial size=3D2></FONT></STRONG> </DIV>
<DIV><FONT face=3DArial size=3D2>Why the use of the inner forall in =
runST?This is=20
not a normal function declaration in mathematics. Since Haskell is=20
Hindley-Milner typed and can't use an inner forall . Why the use an =
inner=20
forall. Has imagination dried up (sorry, if this seems =
impolite)?</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>Thx</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </DIV>
<DIV><FONT face=3DArial size=3D2>Scott</FONT></DIV></BODY></HTML>
------=_NextPart_000_0035_01C245B3.02659730--