On Wed, 10 Feb 2016, Rob Arthan wrote:
ProofPower takes a different approach to this: it uses the compiler's native integers except where logical soundness requires an IntInf, where it uses a type it defines called INTEGER, which has its own operations @+, @-, @* etc. implemented using the operators of Int or IntInf as appropriate (selected at compile-time by using a conditional compilation feature that is built into the way ProofPower packages ML code into documents).
We used to have separate Int vs. IntInf over a few years (2004-2007), but it was so awkward in mixed tool implementations that people knocked at my door and were asking for more uniformity. So I made some tricks to get int = IntInf.int in SML/NJ.
Now I've started to think about separate int types again, but it would probably be a big upheaval in parts of the system that don't have active maintainers.
Since we are about to discontinue SML/NJ altogether, it would allow to remove the above tricks, and not move them over to Poly/ML.
I can unerstand why you are doing that too, but in this case I'm really glad I tried to maintain compatibility, as it meant I already had almost everything I needed to accommodate the proposed change :-).
The reason for thinking about discontinuation of SML/NJ is not its constant annoyance wrt. type errors, but more profane: many Isabelle sessions run out of memory, even basic things like HOL-Library. So the question needs to be revisted seriously in a few weeks on isabelle-dev mailing list -- it will have far-reaching consequences to have just one ML platform.
Makarius