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>
Cc: "Haskell Cafe List" <haskell-cafe@haskell.org>
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">
<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>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> </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> </DIV>
<DIV><FONT face=3DArial size=3D2>So let's come backe to =
runST.</FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </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>)->=20
a</FONT></FONT></DIV>
<DIV><FONT face=3DArial size=3D2></FONT> </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> </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: "Ashley Yakeley" <</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>></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=20
size=3D2>></FONT></DIV>
<DIV><FONT face=3DArial size=3D2>Cc: "Haskell Cafe List" <</FONT><A=20
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 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>> At 2002-08-18 18:19, Scott J. wrote:<BR>> <BR>> =
>A=20
question: s is not a type variable as a isn't it?<BR>> <BR>> Both =
are=20
quantified type variables. But only one of those quantifiers can =
<BR>> be=20
placed at the top level of the expression.<BR>> <BR>> =
runST=20
:: forall a. ((forall s. ST s a) -> a)<BR>> <BR>> > I mean a =
can be=20
of type Integer while s cannot.<BR>> <BR>> Well yes, you can =
specialise=20
"forall a" to Integer. So runST can be <BR>> specialised to this=20
type:<BR>> <BR>> runST ::[special] (forall s. ST s =
Integer)=20
-> Integer<BR>> <BR>> ...whereas you cannot specialise "s" in =
the same=20
way. Think of it in <BR>> terms of logic, if for all a: f(a), then by =
simple=20
specialisation <BR>> f(Integer).<BR>> <BR>> -- <BR>> Ashley =
Yakeley,=20
Seattle WA<BR>> <BR>> </FONT></BODY></HTML>
------=_NextPart_000_0009_01C2473F.0CFB6930--