Specific denotations for pure types
conal at conal.net
Fri Mar 20 19:38:26 EDT 2009
On Fri, Mar 20, 2009 at 3:51 PM, Achim Schneider <barsoap at web.de> wrote:
> Conal Elliott <conal at 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 () = ()
> data Bool = True | False
> , which might, of course, be represented using machine-integers, but
> have ADT semantics.
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".)
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-prime