Re: Specific denotations for pure types

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. I'm fine with IO continuing to be the (non-denotational) "sin bin" until we find more appealing denotationally-founded replacements. 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. - Conal On Sat, Mar 21, 2009 at 8:52 AM, Sittampalam, Ganesh < ganesh.sittampalam@credit-suisse.com> wrote:

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 wrote:

...

Conal Elliott 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

==============================================================================