Re: In precision typing we trust

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

On 2025-08-27 02:00, Paul Rubin wrote:

> F didn't encounter a type error until it tried to do arithmetic on its
> argument.

It didn't encounter error before executing erroneous code... (:-))

> If it instead called its argument based on some decision,
> that wouldn't have been a type error.

Sure. But this is not a type error, it is untyped.

> You don't get to decide whether
> that counts as a type system or not.  It's just a coarser version of Ada
> doing runtime checks on array subscripts and integer overflow,

Wrong. Checking constraints is a defined behavior. The type is defined 
so that exception is a part of the operation's contract. The operation 
is bounded by that contract. In Python the contract of an operation (if 
Python were typed) is an open ended and thus non-existent as such.

> instead
> of statically verifying that they are in range (a proof system like Agda
> would consider those to also be type errors).

Nope, these are not type errors. In a strongly typed language that thing 
does not exist per definition because all type errors are detected at 
compile time.

The discussion was whether this would require weakening the type system 
strength. Python here is really of zero interest.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de