Specific denotations for pure types

[Conal Elliott]

>
> 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-prime/attachments/20090320/08a886a2/attachment.htm