... so I don't think it makes sense to consider (>) a part of Bool's semantics, no?
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
-----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-----