Re: Specific denotations for pure types
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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Specific denotations for pure types
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. -- (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
RE: Specific denotations for pure types
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-boun...@haskell.org [mailto:haskell-prime-boun...@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-boun...@haskell.org [mailto:haskell-prime-boun...@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-su
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 < ganesh.sittampa...@credit-suisse.com> wrote: > Are you proposing to ban all implementation-dependent behaviour > everywhere in Haskell? (Or perhaps relegate it all to IO?) > > -- > *From:* haskell-prime-boun...@haskell.org [mailto: > haskell-prime-boun...@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 > > == > > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: Specific denotations for pure types
Are you proposing to ban all implementation-dependent behaviour everywhere in Haskell? (Or perhaps relegate it all to IO?) From: haskell-prime-boun...@haskell.org [mailto:haskell-prime-boun...@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 === ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Specific denotations for pure types
I now think you've been right all along; Integer should have been the normal numeric type. Of course, Integer is also machine dependent, but you can have larger numbers before everything turns to bottom. The Int type would then be in a implementation dependent library, and would promise the best speed. And for types like Int8, Int16, etc, there should be a number of different types for each of them, because there are at least three different kinds of overflow semantics which are all useful. -- Lennart On Sat, Mar 21, 2009 at 10:49 AM, Jon Fairbairn wrote: > Conal Elliott writes: >> Oh -- not one version of Int for 32-bit execution and another version for >> 64-bit execution? Seen on #haskell today: >> >> > maxBound :: Int >> 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.fairba...@cl.cam.ac.uk > > ___ > Haskell-prime mailing list > Haskell-prime@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-prime > ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Specific denotations for pure types
Conal Elliott writes: > Oh -- not one version of Int for 32-bit execution and another version for > 64-bit execution? Seen on #haskell today: > >> maxBound :: Int > 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.fairba...@cl.cam.ac.uk ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
