[isabelle-dev] Integers in Poly/ML

[Makarius]

On 02/11/16 15:43, Makarius wrote:
> On 02/11/16 15:30, Lawrence Paulson wrote:
> 
> We also have conceptual reasons to stay true to the concept of an
> integer that is an integer, a string that is a string etc. -- and thus
> not using a machine word instead of an integer, or a "char" type that
> cannot hold a textual character (not even in Unicode). Isabelle/ML is
> meant to be a programming environment free from bad jokes like that.

This side-track requires more explanations: recent changes by David
Matthews in Poly/ML provide more direct access to machine word
arithmetic, but also characters that are not the same as singleton
strings (which used to be the representation over 3 decades).

The problem is that type char cannot hold a text entity outside the
ASCII / ISO-LATIN world from the 1980s. Even wide chars from the 1990s
are not sufficient, see the nice article http://utf8everywhere.org -- it
explains why Windows, Java, even Python did it all wrong (while meaning
only good).

This view of varianbe-width characters nicely fits into the Isabelle
symbol representation, as packed strings or exploded strings. And after
some standard fine-tuning of the implementation, the change of
representation in the Poly/ML repository version did not affect Isabelle
performance: we could keep up our model of an unbounded formal alphabet.


	Makarius