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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
