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

Conal Elliott <conal@conal.net> wrote:

> Even the denotation of Bool & () are influenced
> by the denotation of Int, since Bool & () expressions can contain Int
> expressions.
>

Now you've lost me... they definitely shouldn't be. Otherwise, I could
be equally well coding in C.

In my mind, there's somewhere the equivalent of

data () = ()

and

data Bool = True | False

, which might, of course, be represented using machine-integers, but
have ADT semantics.

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. So a semantic domain for Bool and even () would have to include the machine-dependence of Int, so that oops could mean a function from MachineInfo that returns () sometimes and bottom sometimes. If the denotations (semantic domains) for Bool and () didn't include this complexity, they wouldn't be rich enough to capture the machine-dependence of dodgy and oops.

(I'm simplifying by saying "MachineInfo" and "machine-dependence", since apparently the semantics is not fully specified even for a given machine. For instance, the number of tag bits could vary from one compiler or compiler-release to another. Also, Lennart mentions that "as far as I know the overflow/underflow semantics is implementation dependent".)

- Conal