<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML><HEAD>
<META http-equiv=Content-Type content="text/html; charset=us-ascii">
<META content="MSHTML 6.00.2900.3492" name=GENERATOR></HEAD>
<BODY>
<DIV dir=ltr align=left><SPAN class=547025215-21032009><FONT face=Arial 
color=#800000 size=2>Are you proposing to ban all implementation-dependent 
behaviour everywhere in Haskell? (Or perhaps relegate it all to 
IO?)</FONT></SPAN></DIV><BR>
<DIV class=OutlookMessageHeader lang=en-us dir=ltr align=left>
<HR tabIndex=-1>
<FONT face=Tahoma size=2><B>From:</B> haskell-prime-bounces@haskell.org 
[mailto:haskell-prime-bounces@haskell.org] <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> haskell-prime@haskell.org<BR><B>Subject:</B> Re: 
Specific denotations for pure types<BR></FONT><BR></DIV>
<DIV></DIV>
<BLOCKQUOTE class=gmail_quote 
style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">yes, 
  but dodgy isn't Bool, it's _a_ Bool.</BLOCKQUOTE>
<DIV><BR>Right.&nbsp; dodgy is _a_ Bool, and therefore its meaning is an element 
of the meaning of Bool.&nbsp; 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>&nbsp; - Conal<BR></DIV><BR>
<DIV class=gmail_quote>On Fri, Mar 20, 2009 at 5:13 PM, Achim Schneider <SPAN 
dir=ltr>&lt;<A href="mailto:barsoap@web.de">barsoap@web.de</A>&gt;</SPAN> 
wrote:<BR>
<BLOCKQUOTE class=gmail_quote 
style="PADDING-LEFT: 1ex; MARGIN: 0pt 0pt 0pt 0.8ex; BORDER-LEFT: rgb(204,204,204) 1px solid">
  <DIV class=im>Conal Elliott &lt;<A 
  href="mailto:conal@conal.net">conal@conal.net</A>&gt; wrote:<BR><BR></DIV>
  <DIV class=im>&gt; Consider<BR>&gt; &nbsp; &nbsp; big :: Int<BR>&gt; &nbsp; 
  &nbsp; big = 2147483647<BR>&gt; &nbsp; &nbsp; dodgy :: Bool<BR>&gt; &nbsp; 
  &nbsp; dodgy = big + 1 &gt; big<BR>&gt; &nbsp; &nbsp; oops :: ()<BR>&gt; 
  &nbsp; &nbsp; oops = &nbsp;if dodgy then () else undefined<BR>&gt;<BR>&gt; 
  Assuming compositional semantics, the meaning of oops depends on the<BR>&gt; 
  meaning of dodgy, which depends on the meaning of big+1, which is<BR>&gt; 
  implementation-dependent.<BR>&gt;<BR></DIV>yes, but dodgy isn't Bool, it's _a_ 
  Bool. You're worried about the<BR>semantics of (&gt;) :: Int -&gt; Int -&gt; 
  Bool, (+) :: Int -&gt; Int -&gt; Int and<BR>that forall n &gt; 0 . x + n &gt; 
  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 -&gt; Bool. In fact, if you can prove for a certain Bool 
  that<BR>MachineInfo -&gt; 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 class=h5><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">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></BODY></HTML>
<BR/><!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN"><html><p class=MsoNormal><span lang=EN-US style='font-size:8.0pt;font-family:Courier'>==============================================================================<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">http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html</a><br>==============================================================================<o:p></o:p></span></p></html><br>