[isabelle-dev] Integers in Poly/ML

[Makarius]

On 02/11/16 15:37, Tobias Nipkow wrote:
> 
> With bounded integers, we would have to worry about what happens to
> over/underflow exceptions: can handlers for such exceptions in a piece
> of user code lead to unsoundness in the inference system? At first it
> seems that if such an exception propagates out of the kernel, no
> incorrect theorems can arise (because control has left the kernel).
> However, in the presence of higher-order functions (e.g. user functions
> can be passed to kernel code) this is not so clear to me.

This introduces two more aspects:

  (1) Spurious overflow exceptions: our ML code (even out there in user
tools) is usually quite clean, in *not* using unspecific exception
handlers, but that is no guarantee. Interestingly, the SML'97 + SML/NJ
guys who introduced the short ints also propagated the "handle _ => .."
style that makes a programm erratic wrt. environmental effects
(interrupts) and unexpected overflows.

  (2) Critical modules (sometimes called kernel, although we have more
than one such area). Here the exception situation is clean, because the
sources have been inspected over and over again. One benefit of *not*
using full int, but the speculative type "index" for term structures,
would be a simpler situation in the ML implementation. We've had errors
with full integers in distant past, in the glue between the ML and C
world. Relying only on plain machine arithmetic with overflow handling
would reduce the dependence on other modules.


	Makarius