[isabelle-dev] Integers in Poly/ML

[Makarius]

On 02/11/16 15:30, Lawrence Paulson wrote:
> 
> I actually can’t think of many places where Isabelle would need large
> integers, so it would probably benefit even more than MetiTarski does.

"Can't think of" merely indicates a lack of empirical tests, against the
Isabelle repository and AFP. Afterwards the situation usually looks
quite different, and the initial hypothesis needs to be changed.

When we moved to proper int by default some years ago, there were
several tool implementors approaching me, asking to be delivered from
the curse of many different "int" types.

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.


Nonetheless, I do think that proper use of machine words in isolated
situations can help, but they should not be called "int" and used by
default.


	Makarius