Python from Wise Guy's Viewpoint

[Dirk Thierbach]

prunesquallor at comcast.net wrote:
> 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. 

Yes, of course.

> 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.

Hindley-Milner type inference always terminates. The result is either
a provable mismatch, or a provable-non-mismatch.

> My point is that type systems can reject valid programs.

That depends on what you understand by "valid". A provable mismatch
means that there is an execution branch that will crash if you ever
get there. If for some reason this branch will never get executed,
either because it's (non-provably) dead code, or because you have
an implicit restriction for possible arguments to this expression
the type system doesn't know about, than you could call it a "valid
program", but it will still be rejected, yes.

I am still not sure I get your point. (Maybe we always agreed; I just
don't know).

- Dirk