Specific denotations for pure types

[Conal Elliott]

>
> ... 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 <jake at 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-----
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20090323/893bd929/attachment.htm