Are you proposing to ban all implementation-dependent behaviour everywhere in Haskell? (Or perhaps relegate it all to IO?)

---

From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of Conal Elliott
Sent: 21 March 2009 00:56
To: Achim Schneider
Cc: haskell-prime@haskell.org
Subject: Re: Specific denotations for pure types

yes, but dodgy isn't Bool, it's _a_ Bool.

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.

  - Conal

On Fri, Mar 20, 2009 at 5:13 PM, Achim Schneider <barsoap@web.de> wrote:

Conal Elliott <conal@conal.net> wrote:

> Consider
>     big :: Int
>     big = 2147483647
>     dodgy :: Bool
>     dodgy = big + 1 > big
>     oops :: ()
>     oops =  if dodgy then () else undefined
>
> Assuming compositional semantics, the meaning of oops depends on the
> meaning of dodgy, which depends on the meaning of big+1, which is
> implementation-dependent.
>

yes, but dodgy isn't Bool, it's _a_ Bool. You're worried about the
semantics of (>) :: Int -> Int -> Bool, (+) :: Int -> Int -> Int and
that forall n > 0 . x + n > x doesn't hold for Int. There are
infinitely many ways to get a Bool out of things that don't happen to
be Int (not to mention infinitely many ways to get a Bool out of an
Int in an architecture-independent manner), which makes me think it's
quite err... fundamentalistic to generalise that forall Bool .
MachineInfo -> Bool. In fact, if you can prove for a certain Bool that
MachineInfo -> ThatBool, you (most likely) just found a bug in the
program.

Shortly put: All that dodginess is fine with me, as long as it isn't
the only way. Defaulting to machine-independent semantics at the
expense of performance would be a most sensible thing, and Conal
seems to think _way_ too abstractly.

--
(c) this sig last receiving data processing entity. Inspect headers
for copyright history. All rights reserved. Copying, hiring, renting,
performance and/or quoting of this signature prohibited.


_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime

==============================================================================
Please access the attached hyperlink for an important electronic communications disclaimer:
http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html
==============================================================================