Conal Elliott 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. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

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.

yes, but dodgy isn't Bool, it's _a_ Bool. You're worried about the semantics of (>) :: Int -> Int -> Bool, (+) :: Int -> Int -> Int and that forall n > 0 . x + n > x doesn't hold for Int. There are infinitely many ways to get a Bool out of things that don't happen to be Int (not to mention infinitely many ways to get a Bool out of an Int in an architecture-independent manner), which makes me think it's quite err... fundamentalistic to generalise that forall Bool . MachineInfo -> Bool. In fact, if you can prove for a certain Bool that MachineInfo -> ThatBool, you (most likely) just found a bug in the program. Shortly put: All that dodginess is fine with me, as long as it isn't the only way. Defaulting to machine-independent semantics at the expense of performance would be a most sensible thing, and Conal seems to think _way_ too abstractly. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

Are you proposing to ban all implementation-dependent behaviour everywhere in Haskell? (Or perhaps relegate it all to IO?) ________________________________ From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 21 March 2009 00:56 To: Achim Schneider Cc: haskell-prime@haskell.org Subject: Re: Specific denotations for pure types yes, but dodgy isn't Bool, it's _a_ Bool. Right. dodgy is _a_ Bool, and therefore its meaning is an element of the meaning of Bool. If _any_ element of Bool (e.g. dodgy) has a machine-dependent meaning, then the meaning of Bool itself much have a complex enough structure to contain such an element. - Conal On Fri, Mar 20, 2009 at 5:13 PM, Achim Schneider wrote: 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. > yes, but dodgy isn't Bool, it's _a_ Bool. You're worried about the semantics of (>) :: Int -> Int -> Bool, (+) :: Int -> Int -> Int and that forall n > 0 . x + n > x doesn't hold for Int. There are infinitely many ways to get a Bool out of things that don't happen to be Int (not to mention infinitely many ways to get a Bool out of an Int in an architecture-independent manner), which makes me think it's quite err... fundamentalistic to generalise that forall Bool . MachineInfo -> Bool. In fact, if you can prove for a certain Bool that MachineInfo -> ThatBool, you (most likely) just found a bug in the program. Shortly put: All that dodginess is fine with me, as long as it isn't the only way. Defaulting to machine-independent semantics at the expense of performance would be a most sensible thing, and Conal seems to think _way_ too abstractly. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================

I'm having trouble understanding the scope of what you're proposing. The Haskell standard defines various pure types, and it seems that you want all those types to be completely defined. But what about types that aren't in the Haskell standard? Are implementations allowed to add their own types too (e.g. Int under a new name) which are machine-dependent? If they do, then you can still make elements of Bool that are machine-dependent. ________________________________ From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 21 March 2009 18:15 To: Sittampalam, Ganesh Cc: Achim Schneider; haskell-prime@haskell.org Subject: Re: Specific denotations for pure types I'm suggesting that we have well-defined denotations for the pure types in Haskell, and that the various Haskell implementations be expected to implement those denotations. I'm fine with IO continuing to be the (non-denotational) "sin bin" until we find more appealing denotationally-founded replacements. I didn't answer your question as stated because I don't know what you include in "behaviour" for a functional program. I have operational associations with that word. - Conal On Sat, Mar 21, 2009 at 8:52 AM, Sittampalam, Ganesh wrote: Are you proposing to ban all implementation-dependent behaviour everywhere in Haskell? (Or perhaps relegate it all to IO?) ________________________________ From: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of Conal Elliott Sent: 21 March 2009 00:56 To: Achim Schneider Cc: haskell-prime@haskell.org Subject: Re: Specific denotations for pure types yes, but dodgy isn't Bool, it's _a_ Bool. Right. dodgy is _a_ Bool, and therefore its meaning is an element of the meaning of Bool. If _any_ element of Bool (e.g. dodgy) has a machine-dependent meaning, then the meaning of Bool itself much have a complex enough structure to contain such an element. - Conal On Fri, Mar 20, 2009 at 5:13 PM, Achim Schneider wrote: 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. > yes, but dodgy isn't Bool, it's _a_ Bool. You're worried about the semantics of (>) :: Int -> Int -> Bool, (+) :: Int -> Int -> Int and that forall n > 0 . x + n > x doesn't hold for Int. There are infinitely many ways to get a Bool out of things that don't happen to be Int (not to mention infinitely many ways to get a Bool out of an Int in an architecture-independent manner), which makes me think it's quite err... fundamentalistic to generalise that forall Bool . MachineInfo -> Bool. In fact, if you can prove for a certain Bool that MachineInfo -> ThatBool, you (most likely) just found a bug in the program. Shortly put: All that dodginess is fine with me, as long as it isn't the only way. Defaulting to machine-independent semantics at the expense of performance would be a most sensible thing, and Conal seems to think _way_ too abstractly. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited. _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ======================================================================== ====== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ======================================================================== ====== =============================================================================== Please access the attached hyperlink for an important electronic communications disclaimer: http://www.credit-suisse.com/legal/en/disclaimer_email_ib.html ===============================================================================

Duncan Coutts wrote:

The question is what should we do about it, if anything? A certain amount of machine dependent behaviour would seem to be useful. Even machine-dependent Int it's not in the H98 standard, implementations would want to add it as an efficiency extension and then we're back to the same place because one machine-dependent type infects all types.

I think defining a platform-independent core would be useful, not only from an engineering perspective. Having the semantics defined for the bulk of the language is better than having none or an unnecessarily complex one. If you then really want to, you can always instantiate the semantics to the platform you're using, adding Int and friends, but not delving down into the MachineInfo -> realm, which no implementation is going to use, anyway: I've yet to see a Haskell implementation that allows one program to be run across multiple processors of e.g. different bitsizes, and if it existed, it'd most likely limit any sane use to that platform-independent core. Thinking about GPU's, different FPE exception models and all that punk, I guess we'd have CReal as platform-independent, IEEEFloat/IEEEDouble as platform-independent-as-long-as-you-don't-blow-them-up, and Float/Double as not even necessarily providing IEEE semantics. -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

On Sat, Mar 21, 2009 at 12:08 PM, Achim Schneider wrote:

Conal Elliott wrote:

...

...

yes, but dodgy isn't Bool, it's _a_ Bool.

Right. dodgy is _a_ Bool, and therefore its meaning is an element of the meaning of Bool. If _any_ element of Bool (e.g. dodgy) has a machine-dependent meaning, then the meaning of Bool itself much have a complex enough structure to contain such an element.

Then, yes, every Haskell type depends on whatever any type depends on, and the only way for the denotations not to explode into one's face is to abstract away the fact that an expression forces its context upon its continuation. "MachineInfo ->" can be added by the denotation of function application, there's no need to have it inside Bool's denotation.

Maybe what you're saying is that the meanings of the strictly boolean building blocks (True, False, &&, ||, not) don't do anything interesting with machine-info. They just pass it along in a totally standard way that can be abstracted out. If so, I agree. And still, dodgy does have type Bool, so the meaning of Bool (the corresponding semantic domain) must have room in it for the meaning of dodgy, i.e., for machine-dependence (and compiler-dependence). The principle I'm assuming is that the meaning of a well-typed expression inhabits the meaning of the expression's type. (BTW, this principle explains what's unsafe about unsafePerformIO.) - Conal

... 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 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-----

Oh! I think there's a misunderstanding here. I'm not talking about MachineInfo as visible in the types. I'm talking about Int itself having a MachineInfo-dependent semantic model (something like MachineInfo -> Z, where MachineInfo, ->, and Z are *semantic* types, not Haskell types). Making my question more specific: Can (>) on Int be given a compositional semantics, i.e. a semantics as [[Int]] -> [[Int]] -> [[Bool]], where [[Int]] = MachineInfo -> Z and [[Bool]] = {bottom,false,true} (with the usual ordering)? - Conal On Mon, Mar 23, 2009 at 9:34 AM, Jake McArthur wrote:

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

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

As I understand it, your question might be reworded like this: If we can compose values of type (MachineInfo -> Int) to create a value of type (MachineInfo -> Bool), does that mean Bool is dependent on MachineInfo? To simplify the question, I would like to rephrase it further to ask whether the ability to construct any value of type (MachineInfo -> Bool) means that Bool is dependent on MachineInfo. My (uneducated) reaction is that this does not mean that Bool is dependent on MachineInfo any more than the ability to construct a value of type (forall a. a -> Bool) means that Bool is dependent on everything.

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

iEYEARECAAYFAknHufsACgkQye5hVyvIUKnahACgq6JZLcSePAJ4RLylPyz3X2DC NwMAoLQilWKYfUf12BJhUle52bP/zM2J =NN7V -----END PGP SIGNATURE-----

Int provides minimum of -2^29..2^29-1, and as far as I know the overflow/underflow semantics is implementation dependent. Personally, I try to use Integer, unless I'm forced to use Int. -- Lennart On Fri, Mar 20, 2009 at 11:17 PM, Achim Schneider wrote:

Conal Elliott wrote:

...

I'd always assumed that pure (non-imperative) types have specific denotational models, so that for instance the denotation of something of type Int is either bottom or a (smallish) integer.

IIRC, Ints provide signed modulo at-least-31 bits arithmetic, which is a clearly defined, but still utterly under-specified semantic. The idea is that if you want to be safe, you can just use Integer and only be bounded by the implementation's address width and swap space (I heard that Integers break at MAX_INT^MAX_INT). The other idea is that Int is a number type small enough to be as fast as possible, which, in practise, means "fits into a register, together with some tag", which excuses Int's existence where Int32 and Int64 are around.

I'm all for defaulting to Integer and providing Natural (as an potentially-unbounded alternative to Nat, which'd be one bit wider than Int)... the (usually meagre) performance gains you can get by choosing Int over Integer are worth an explicit type annotation, and with Integer, you get non-modulo semantics, by default. Is that what you want?

-- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

On Fri, Mar 20, 2009 at 6:11 PM, John Meacham wrote:

...

I just learned on #haskell that Int has implementation/machine-dependent semantics. I'd always assumed that pure (non-imperative) types have specific denotational models, so that for instance the denotation of something of type Int is either bottom or a (smallish) integer. Since precise & simple denotation is at the heart of how I think about programming, and Haskell is my favorite language, I'm startled and disappointed. I knew we didn't have a denotational semantics for Haskell, but I'd previously assumed it was just a matter of working out the

On Fri, Mar 20, 2009 at 12:02:15PM -0700, Conal Elliott wrote: details.

in jhc and ghc at least, they are expressed directly in haskell as standard data types with a single unboxed component.

...

data Int = I Bits32_

Where Bits32_ is a direct unboxed representation of a 32 bit quantity. The data declaration behaves just like any other haskell data declaration and hence follows the same lazy semantics. Of course, this may not help as you perhaps need to define the meaning of the unboxed value inside the Int box, but it at least seperates the 'lazy' aspect of Int from its underlying representation and primitives.

John

Oh -- not one version of Int for 32-bit execution and another version for 64-bit execution? Seen on #haskell today: <mux> > maxBound :: Int

<lambdabot> 9223372036854775807

- Conal

Conal Elliott writes:

Oh -- not one version of Int for 32-bit execution and another version for 64-bit execution?  Seen on #haskell today:

<mux> > maxBound :: Int <lambdabot>   9223372036854775807

I've always been opposed to having Int "built in" (in contrast to having Int32 and Int64 defined in a library somewhere). It's much cleaner to have Integer as the language integer. A reference implementation of Int8 (for brevity!) could be written with (off the top of my head) data Int8 = Int8 !Bool !Bool !Bool !Bool !Bool !Bool !Bool !Bool which would specify the semantics exactly. -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk