Re: In precision typing we trust

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

On 2025-08-31 00:25, Lawrence D’Oliveiro wrote:
> On Fri, 29 Aug 2025 10:15:56 +0200, Dmitry A. Kazakov wrote:
> 
>> On 2025-08-29 05:54, Lawrence D’Oliveiro wrote:
>>>
>>> On Thu, 28 Aug 2025 11:43:15 +0200, Dmitry A. Kazakov wrote:
>>>
>>>> In Python everything is untyped even when type annotations are used.
>>>
>>>       Python 3.13.7 (main, Aug 20 2025, 22:17:40) [GCC 14.3.0] on linux
>>>       Type "help", "copyright", "credits" or "license" for more information.
>>>       >>> 2 + "2"
>>>       Traceback (most recent call last):
>>>         File "<python-input-0>", line 1, in <module>
>>>           2 + "2"
>>>           ~~^~~~~
>>>       TypeError: unsupported operand type(s) for +: 'int' and 'str'
>>
>> "+" is implemented to raise an exception named TypeError. So? How is
>> that a type check?
> 
> You mean it doesn’t do type checking in Ada??

I mean that no type check is made in Python. Naming exception TypeError 
does not mean type error.

>> How do I know if that happens without executing "+"?
> 
> Look at the definitions of the classes involved.

What "look" does formally mean and why Python didn't do it?

>> It is just untyped as no types of "+" are specified anywhere.
> 
> They are in the classes that implement that operator.

Can you list them? No? Then see above "no types of "+" are specified 
anywhere."

>> It is an undefined behavior ...
> 
> It is defined in the classes that implement that operator.

q.e.d.

It is undefined in the classes that do not implement that operator => On 
all classes it is undefined.

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