<div dir="ltr"><div class="gmail_quote"><div class="im">On Thu, Aug 8, 2013 at 7:40 AM, Timon Gehr <span dir="ltr">&lt;<a href="mailto:timon.gehr@gmx.ch" target="_blank">timon.gehr@gmx.ch</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">


<div>
You make the distinction between &quot;evaluate&quot;,<br>
</div></blockquote>
<br>
Which essentially means applying reduction rules to an expression until the result is a value.<div><br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
and  &quot;execute&quot; or &quot;run&quot;, etc. This is not functional.<br>
</blockquote>
<br></div>
How would you know?<br></blockquote><div><br></div></div><div>I think 
Jerzy is alluding to the fact that we don&#39;t have a denotational 
semantics for IO. So I&#39;m not sure I understand your response. Are you 
pointing out that some subspace of IO programs admit such a semantics 
via an easy inspection?<br>
<br></div><div class="im"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">&#39;putStr &quot;c&quot;&#39; is a pure value. </blockquote></div></div>

<br><div class="gmail_extra">
This is the crux of the matter: &quot;pure value&quot; means different things to different people.<br><br>Some employ it to mean an effectful monadic expression to distinguish between getLine and (return &quot;Hello&quot;), both of type IO String.<br>


<br></div><div class="gmail_extra">Others use it to distinguish between an ordinary Haskell expression and, say, C.<br><br></div><div class="im"><div class="gmail_extra">So when you write:<br><br>&gt; 
&#39;unsafePerformIO (putStr &quot;c&quot;)&#39; is not a pure value.<br><br></div></div>I infer you&#39;re in the latter camp.<br><br>Would you then speak of &#39;effectful&#39; values vs &#39;null-effectful&#39; ones? What oral syntax would you actually use?</div>

<div class="gmail_extra"><br clear="all"><div>-- Kim-Ee</div>
<br><br><div class="gmail_quote">On Thu, Aug 8, 2013 at 7:40 AM, Timon Gehr <span dir="ltr">&lt;<a href="mailto:timon.gehr@gmx.ch" target="_blank">timon.gehr@gmx.ch</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

<div class="im">On 08/08/2013 01:19 AM, Jerzy Karczmarczuk wrote:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
Bardur Arantsson comments the comment of Joe Quinn:<br>
</div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">


&gt;On 8/7/2013 11:00 AM, David Thomas wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
&gt;&gt;twice :: IO () -&gt; IO ()<br>
&gt;&gt;twice x = x &gt;&gt; x<br>
&gt;&gt;<br>
&gt;&gt;I would call that evaluating x twice (incidentally creating two<br>
&gt;&gt;separate evaluations of one pure action description), but I&#39;d like to<br>
&gt;&gt;better see your perspective here.<br>
</blockquote>
&gt;<br></div>
&gt;x is only evaluated once, but/executed/  twice. For IO, that means<div class="im"><br>
&gt;magic. For other types, it means different things. For Identity, twice =<br>
&gt;id!<br>
&gt;<br>
</div></blockquote><div class="im">
Your point being? x is the same thing regardless of how many times you<br>
run it.<br>
</div></blockquote><div class="im">
<br>
What do you mean by &quot;the same thing&quot;? You cannot compare &#39;them&#39; in any<br>
reasonable sense.<br></div>
...<br>
</blockquote>
<br>
<a href="http://en.wikipedia.org/wiki/Identity_of_indiscernibles" target="_blank">http://en.wikipedia.org/wiki/<u></u>Identity_of_indiscernibles</a><br>
<br>
(He is reasoning _about_ the language and not _within_ the language because Haskell does not support very powerful reasoning internally.)<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
...<div class="im"><br>
You make the distinction between &quot;evaluate&quot;,<br>
</div></blockquote>
<br>
Which essentially means applying reduction rules to an expression until the result is a value.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
and  &quot;execute&quot; or &quot;run&quot;, etc. This is not functional.<br>
</blockquote>
<br></div>
How would you know?<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
Your program doesn&#39;t &quot;run&quot; anything, it<br>
applies (&gt;&gt;=) (or equivalent) to an IO (...) object. This is the only<br>
&quot;practical evaluation&quot; of it, otherwise it can  be passed (or duplicated<br>
as above). But you cannot apply &quot;bind&quot; twice to the same instance of it<br>
(in fact, as I said above, &quot;the same instance&quot;  is a bit suspicious<br>
concept...).<br></div>
...<br>
</blockquote>
<br>
Indeed, but you didn&#39;t say that above.<div class="im"><br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
The &quot;running&quot; or &quot;execution&quot; takes place outside of your program. In<br>
such a way Richard O&#39;Keefe and I converge... That&#39;s why I say that the<br>
concept of purity is meaningless in the discussed context.<br>
</blockquote>
<br></div>
Not meaningless, but redundant. The point of having a purely functional programming language is to have reasoning based on purity be universally applicable.<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="im">
It is a kind of counterfeit notion, inherited from &quot;pure functions&quot; to something<br>
which belongs to two different worlds.<br></div>
...<br>
</blockquote>
<br>
&#39;putStr &quot;c&quot;&#39; is a pure value.<br>
<br>
On the other hand:<br>
<br>
&#39;unsafePerformIO (putStr &quot;c&quot;)&#39; is not a pure value.<br>
<br>
(But this expression does not exist in standard Haskell. unsafePerformIO &quot;unquotes&quot; the action. You may be confusing the &quot;quoted&quot; and &quot;unquoted&quot; versions.)<div class="HOEnZb"><div class="h5">

<br>
<br>
<br>
______________________________<u></u>_________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/<u></u>mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br></div>