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