What I want is a specific, simple language-defined denotation for Haskell's pure types and for pure expressions having those types.

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 ->' ?

  - Conal

On Fri, Mar 20, 2009 at 3:17 PM, Achim Schneider <barsoap@web.de> wrote:
Conal Elliott <conal@conal.net> wrote:

> I'd always assumed that pure (non-imperative) types have
> specific denotational models, so that for instance the denotation of
> something of type Int is either bottom or a (smallish) integer.
>
IIRC, Ints provide signed modulo at-least-31 bits arithmetic, which is a
clearly defined, but still utterly under-specified semantic. The idea
is that if you want to be safe, you can just use Integer and only be
bounded by the implementation's address width and swap space (I heard
that Integers break at MAX_INT^MAX_INT). The other idea is that Int is
a number type small enough to be as fast as possible, which, in
practise, means "fits into a register, together with some tag", which
excuses Int's existence where Int32 and Int64 are around.

I'm all for defaulting to Integer and providing Natural (as an
potentially-unbounded alternative to Nat, which'd be one bit wider than
Int)... the (usually meagre) performance gains you can get by choosing
Int over Integer are worth an explicit type annotation, and with
Integer, you get non-modulo semantics, by default. Is that what you
want?

--
(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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime