What I want is a specific, simple language-defined denotation for Haskell's pure types and for pure expressions having those types.<br><br>I guess currently the denotation of Int is something like 'MachineInfo -> Z + bottom' rather than the Z+bottom I thought it was. Or, to remove the junk values, some kind of dependent type 'Pi info :: WadOfMachineInfo -> Int info + bottom', vs a type like Z32+bottom. Similarly for other pure (not as pure as I thought) types. Even the denotation of Bool & () are influenced by the denotation of Int, since Bool & () expressions can contain Int expressions. Does the (denotational) semantics of every Haskell type indeed include 'MachineInfo ->' ?<br>
<br> - Conal<br><br><div class="gmail_quote">On Fri, Mar 20, 2009 at 3:17 PM, Achim Schneider <span dir="ltr"><<a href="mailto:barsoap@web.de">barsoap@web.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
<div class="im">Conal Elliott <<a href="mailto:conal@conal.net">conal@conal.net</a>> wrote:<br>
<br>
> I'd always assumed that pure (non-imperative) types have<br>
> specific denotational models, so that for instance the denotation of<br>
> something of type Int is either bottom or a (smallish) integer.<br>
><br>
</div>IIRC, Ints provide signed modulo at-least-31 bits arithmetic, which is a<br>
clearly defined, but still utterly under-specified semantic. The idea<br>
is that if you want to be safe, you can just use Integer and only be<br>
bounded by the implementation's address width and swap space (I heard<br>
that Integers break at MAX_INT^MAX_INT). The other idea is that Int is<br>
a number type small enough to be as fast as possible, which, in<br>
practise, means "fits into a register, together with some tag", which<br>
excuses Int's existence where Int32 and Int64 are around.<br>
<br>
I'm all for defaulting to Integer and providing Natural (as an<br>
potentially-unbounded alternative to Nat, which'd be one bit wider than<br>
Int)... the (usually meagre) performance gains you can get by choosing<br>
Int over Integer are worth an explicit type annotation, and with<br>
Integer, you get non-modulo semantics, by default. Is that what you<br>
want?<br>
<br>
--<br>
(c) this sig last receiving data processing entity. Inspect headers<br>
for copyright history. All rights reserved. Copying, hiring, renting,<br>
performance and/or quoting of this signature prohibited.<br>
<br>
<br>
_______________________________________________<br>
Haskell-prime mailing list<br>
<a href="mailto:Haskell-prime@haskell.org">Haskell-prime@haskell.org</a><br>
<a href="http://www.haskell.org/mailman/listinfo/haskell-prime" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-prime</a><br>
</blockquote></div><br>