Specific denotations for pure types

[Sittampalam, Ganesh]

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/f1058a1d/attachment.htm