[Types-sig] how to do a typecase? (was: Static typing: Towards closure?)

[Tim Peters]

[Jeremy Hylton]
> My argument restated briefly is that we should clearly specify
> the type system for Python, so that we can verify that
> typecheckers faithfully implement the type rules.

[John Skaller]
> 	And my response is: what you are calling for is not
> mathematically possible. You are aware of the halting
> problem [a restatement of Goedels theorem in a computing
> context]? There is an analog for type systems.  The theorem
> says that any sufficiently rich type system cannot be checked:
> finding a 'complete' checker is analogous to finding an
> algorithm that tells if a program terminates. [Every 'checker'
> will fail on some cases, either explicitly, or by looping for
> ever.]

Proving the *equivalence* of two distinct typecheckers is nevertheless not
precluded by the (presumed(*)) unsolvability of the typechecking problem.  A
clean analogy is to proof procedures for first-order logic, where several
distinct (sound and complete, but not effective -- it's unsolvable in
general) procedures are known to be equivalent.  As a ridiculous example,
take a typechecker (or theorem prover) written in C and add the line
"(void)42;" at the start of main().  Different program, trivially
equivalent.  Proving equivalence may be harder in other cases <wink>.

No matter how hard the problem is, there's nothing to prevent Python from
specifying *a* typechecking algorithm, then insisting that all Python
typecheckers be equivalent to it.  That would satisfy Jeremy's key (&
reasonable!) requirement:

    If a program checks out with one implementation and not
    with another, then one of the type checkers has a bug!

That is, if typechecker A doesn't do what the reference algorithm does, A is
buggy -- not by virtue of hard thought, but simply by decree.

(*) About "(presumed)":  any number of languages, from Algol to Eiffel, have
effective type-checking procedures (albeit that the fancier ones may, on
occasion, delay a check to runtime, under well-defined circumstances).  I
expect you're using the word "check" where most of the world uses
"inference" instead; e.g., your

    def f():
        return f

example is not a typechecking problem in my eyes (although it is an
inference problem);

    def f() -> T:
        return f

for some specific & explicit T would be what I call a typechecking problem.
I'm not sure what Jeremy means.

> ...
> 	I agree completely with you when you say the type system
> should be clearly stated.

Ir would be hard to disagree with that one <wink>.

> But the semantics for 'ill typed program' should be 'undefined'.
> If you are silly enough to specify behaviour, then you are
> allowing ill typed programs to have well defined meanings.
> (which is absurd).

Then I guess most languages on earth are "silly" wrt their type systems.

granting-the-point-but-not-the-judgment-ly y'rs  - tim