[Types-sig] Conformance model

[Tim Hochberg]

John Skaller wrote:
<SNIP>
> My argument is that this is what should be
> specified for some other 'errors' in some
> contexts. Given that python is dynamic,
> my argument is that, say, for a type error,
> it might make sense to ALLOW:
>
> try:
> 1 + "Hello"
> except TypeError: pass
>
> but mandate that
>
> def f(x):
> 1 + "Hello"
>
> is not a valid Python program -- a compiler
> can reject the program, rather than being
> forced to implement:
>
> def f(x):
> raise TypeError
>
> which is what is currently required.
>
> in particular, most people who use
> compilers RELY on the compiler, when it rejects
> code, NOT providing a .o file, which prevents
> the linker linking the code, which prevents
> the 'erroneous' code actually being run.

Let me stop lurking for a moment to comment:

First off, the function 'f' is close enough to:

def g(x):
    return g + "Hello"

that it strikes me as somewhat strange to ban the former but not the later.
I would like the compiler to catch, report, and reject a file containing the
definition of f(x) when invoked directly (e.g., from the command line) .
However, when invoked implicitly (e.g., by import) the compiler would go
ahead and compile f(x) to raise a type error.

In any event, I fail to see where you gain an efficiency advantage by
outlawing f(x). Perhaps someone can elighten me here. Don't get me wrong, I
definately see the advantage of having f(x) reported by a compiler. And I
see the advantage of not generating .o files by default when invoked from
the command line.

This has finally made me appreicate where Paul Prescod was going with
typesafe. I haven't gone back and reread it, so I apologize if I'm messsing
this up. Anyway, it seems that both:

typesafe
def f(x):
    return 1 + "hello"

typesafe
def g(x):
     return g + "Hello"

would both result in compile time errors similar to SyntaxError. (It
probably should not be TypeError -- TypeError allready has a runtime
meaning, perhaps InterfaceError or StaticTypeError). This, it seems, would
allow more efficient code to be generated (at the very least, checks for
thrown TypeErrors could be removed).

In fact, I would argue that:

def h(x) -> Int:
    return "spam"

should also be legal Python (in some sense), although I would like the
compiler to catch it by default. However:

typesafe
def h(x) -> Int:
    return "spam"

would again raise a compile time error.

<snip>


-tim

PS, I just realized that typesafe is equivalent to a " throws
everythingButTypeError" clause in Java. Doubt it's too important, but I
thought it interesting.