Are you proposing to ban all implementation-dependent behaviour everywhere in Haskell? (Or perhaps relegate it all to IO?)
________________________________ From: haskell-prime-boun...@haskell.org [mailto:haskell-prime-boun...@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 <bars...@web.de> wrote: Conal Elliott <co...@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 ===============================================================================
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
