A denotational semantic definition for a type (more traditionally, a syntactic category) have two parts: a semantic domain and a collection of *compositional* definitions for the building blocks of that type. ("Compositional" in that a construct is defined strictly in terms of the meanings of its components.) I think you're talking about the latter, while my complexity claim is about the former: What semantic model can we have for Bool, i.e. what is [[Bool]]? The model I'd like in a lazy functional language is the domain containing exactly three elements: true, false, and bottom (with the usual information ordering).

Whatever the domain corresponding to Bool is, the denotation of every (well-formed) Bool expression is an element of that domain.

The question I'm asking is this: Assuming compositional semantics, can [[Bool]] be this simple & customary three-value domain in the presence of an implementation-dependent [[Int]] (given that Int expressions can play a non-trivial role in Bool expressions)?

(Now you might say that Bool is just a data type definition. If so, then rephrase the question in terms of simple data type definitions.)

- Conal

On Mon, Mar 23, 2009 at 7:54 AM, Jake McArthur <jake@pikewerks.com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

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

Since Bool's constructors are exported, we can define (>) anywhere, so I
don't think it makes sense to consider (>) a part of Bool's semantics, no?

- - Jake McArthur
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.9 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iEYEARECAAYFAknHoq4ACgkQye5hVyvIUKkRugCghgh6qNqmpWvD5SQYX/8PzUws
0Y8AoM3qJS5RIzoEFbD2aN1rR6EdJWh9
=ozCQ
-----END PGP SIGNATURE-----