Specific denotations for pure types

Achim Schneider barsoap at web.de
Fri Mar 20 18:17:07 EDT 2009


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.




More information about the Haskell-prime mailing list