Specific denotations for pure types

[Conal Elliott]

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 () = ()
>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20090320/4f7b9aa9/attachment.htm