Specific denotations for pure types
Conal Elliott
conal at conal.net
Mon Mar 23 11:54:07 EDT 2009
>
> ... 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
More information about the Haskell-prime
mailing list