On Fri, Mar 20, 2009 at 3:51 PM, Achim Schneider <bars...@web.de> wrote:
> Conal Elliott <co...@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
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
