Specific denotations for pure types

[Conal Elliott]

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 at web.de> wrote:

> Conal Elliott <conal at 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 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/0cf5056a/attachment.htm