I'm suggesting that we have well-defined denotations for the pure types in Haskell, and that the various Haskell implementations be expected to implement those denotations.<br><br>I'm fine with IO continuing to be the (non-denotational) "sin bin" until we find more appealing denotationally-founded replacements.<br>
<br>I didn't answer your question as stated because I don't know what you include in "behaviour" for a functional program. I have operational associations with that word.<br><br> - Conal<br><br><div class="gmail_quote">
On Sat, Mar 21, 2009 at 8:52 AM, Sittampalam, Ganesh <span dir="ltr"><<a href="mailto:ganesh.sittampalam@credit-suisse.com" target="_blank">ganesh.sittampalam@credit-suisse.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div>
<div dir="ltr" align="left"><span><font color="#800000" size="2" face="Arial">Are you proposing to ban all implementation-dependent
behaviour everywhere in Haskell? (Or perhaps relegate it all to
IO?)</font></span></div><br>
<div dir="ltr" align="left" lang="en-us">
<hr>
<font size="2" face="Tahoma"><b>From:</b> <a href="mailto:haskell-prime-bounces@haskell.org" target="_blank">haskell-prime-bounces@haskell.org</a>
[mailto:<a href="mailto:haskell-prime-bounces@haskell.org" target="_blank">haskell-prime-bounces@haskell.org</a>] <b>On Behalf Of </b>Conal
Elliott<br><b>Sent:</b> 21 March 2009 00:56<br><b>To:</b> Achim
Schneider<br><b>Cc:</b> <a href="mailto:haskell-prime@haskell.org" target="_blank">haskell-prime@haskell.org</a><br><b>Subject:</b> Re:
Specific denotations for pure types<br></font><br></div><div><div></div><div>
<div></div>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">yes,
but dodgy isn't Bool, it's _a_ Bool.</blockquote>
<div><br>Right. dodgy is _a_ Bool, and therefore its meaning is an element
of the meaning of Bool. If _any_ element of Bool (e.g. dodgy) has a
machine-dependent meaning, then the meaning of Bool itself much have a complex
enough structure to contain such an element.<br><br> - Conal<br></div><br>
<div class="gmail_quote">On Fri, Mar 20, 2009 at 5:13 PM, Achim Schneider <span dir="ltr"><<a href="mailto:barsoap@web.de" target="_blank">barsoap@web.de</a>></span>
wrote:<br>
<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div>Conal Elliott <<a href="mailto:conal@conal.net" target="_blank">conal@conal.net</a>> wrote:<br><br></div>
<div>> Consider<br>> big :: Int<br>>
big = 2147483647<br>> dodgy :: Bool<br>>
dodgy = big + 1 > big<br>> oops :: ()<br>>
oops = if dodgy then () else undefined<br>><br>>
Assuming compositional semantics, the meaning of oops depends on the<br>>
meaning of dodgy, which depends on the meaning of big+1, which is<br>>
implementation-dependent.<br>><br></div>yes, but dodgy isn't Bool, it's _a_
Bool. You're worried about the<br>semantics of (>) :: Int -> Int ->
Bool, (+) :: Int -> Int -> Int and<br>that forall n > 0 . x + n >
x doesn't hold for Int. There are<br>infinitely many ways to get a Bool out of
things that don't happen to<br>be Int (not to mention infinitely many ways to
get a Bool out of an<br>Int in an architecture-independent manner), which
makes me think it's<br>quite err... fundamentalistic to generalise that forall
Bool .<br>MachineInfo -> Bool. In fact, if you can prove for a certain Bool
that<br>MachineInfo -> ThatBool, you (most likely) just found a bug in
the<br>program.<br><br>Shortly put: All that dodginess is fine with me, as
long as it isn't<br>the only way. Defaulting to machine-independent semantics
at the<br>expense of performance would be a most sensible thing, and
Conal<br>seems to think _way_ too abstractly.<br>
<div>
<div></div>
<div><br>--<br>(c) this sig last receiving data processing entity.
Inspect headers<br>for copyright history. All rights reserved. Copying,
hiring, renting,<br>performance and/or quoting of this signature
prohibited.<br><br><br>_______________________________________________<br>Haskell-prime
mailing list<br><a href="mailto:Haskell-prime@haskell.org" target="_blank">Haskell-prime@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-prime" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-prime</a><br>
</div></div></blockquote></div><br></div></div></div>
<br><p><span style="font-size: 8pt; font-family: Courier;" lang="EN-US">==============================================================================<br>Please access the attached hyperlink for an important electronic communications disclaimer:<br>
<a href="http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html" target="_blank">http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html</a><br>==============================================================================</span></p>
<br>
</blockquote></div><br>