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 <bars...@web.de> wrote: > Conal Elliott <co...@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 >
_______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
