Specific denotations for pure types

[Sittampalam, Ganesh]

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 at haskell.org
[mailto:haskell-prime-bounces at haskell.org] On Behalf Of Conal Elliott
Sent: 21 March 2009 18:15
To: Sittampalam, Ganesh
Cc: Achim Schneider; haskell-prime at 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
<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
	
========================================================================
======




=============================================================================== 
 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/1c7b4de2/attachment-0001.htm