Python from Wise Guy's Viewpoint

[prunesquallor at comcast.net]

Dirk Thierbach <dthierbach at gmx.de> writes:

> prunesquallor at comcast.net wrote:
>> Dirk Thierbach <dthierbach at gmx.de> writes:
>
>>> Now why does a type system reject a program? Because there's a type
>>> mismatch in some branch if the program.
>
>> *or* because the type system was unable to prove that there *isn't* a
>> type mismatch in *all* branches.
>
> I am not sure if I read this correctly, but it seems equivalent to what
> I say.
>
>   \exists branch. mismatch-in (branch)
>
> should be the same as
>
>   \not \forall branch. \not mismatch-in (branch)
>
> Anyway, I don't understand your point.

Only if you assume binary logic. If there are three values that
can arise --- provable-mismatch, provable-non-mismatch, and undecided
--- then you cannot assume that ~provable-mismatch = provable-non-mismatch.

My point is that type systems can reject valid programs.