PEP 3107 and stronger typing (note: probably a newbie question)

[Diez B. Roggisch]

Paul Rubin schrieb:
> "Diez B. Roggisch" <deets at nospam.web.de> writes:
>>> Which implies that even in ADA, runtime type errors are in fact
>>> expected - else there would be no handler for such a case.
>> Well, yes, runtime errors occur - in statically typed languages as
>> well. That's essentially the halting-problem.
> 
> Well, no, it's quite possible for a language to reject every program
> that has any possibility of throwing a runtime type error.  The
> halting problem implies that no algorithm can tell EXACTLY which
> programs throw errors and which do not.  So the language cannot accept
> all programs that are free of runtime type errors and reject all
> programs that definitely have runtime type errors, with no uncertain
> cases.  But it's fine for a language to reject uncertain cases and
> accept only those which it can rigorously demonstrate have no type
> errors.

Sure. But which class of programs are decidable? There's lot's of 
research going on with model checking and the like. But AFAIK, the 
consensus is that the very moment you allow recursive types, the 
type-checking is either incomplete, or possibly non-deterministic. Which 
makes then the compiler hang.

Diez