> > 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 >
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
