Specific denotations for pure types

[Conal Elliott]

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.sittampalam at 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-bounces at haskell.org [mailto:
> haskell-prime-bounces at haskell.org] *On Behalf Of *Conal Elliott
> *Sent:* 21 March 2009 00:56
> *To:* Achim Schneider
> *Cc:* haskell-prime at 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 <barsoap at web.de> wrote:
>
>> Conal Elliott <conal at conal.net> 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 at 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
>
> ==============================================================================
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20090321/033dcbdb/attachment.htm