Hacker News Reader

Comment by 2h | Hacker News Reader

the problem is not type hinting. the problem is people trying to use a single function for any type. as can be seen in the article, that is extremely difficult and error prone. so just dont do that:

    def slow_add(a: int, b: int) -> int:
    def slow_add_float(a: float, b: float) -> float:

OK its not as elegant or pretty, but its really clear what is going on. the problems described in the article crop up because people are trying to have the interpreter intuit what the programmer is wanting, when what the programmer is wanting might be ill defined or simply invalid.

View on HN

So because the type system is far far far far less polymorphic than the underlying code, we're to monomorphize the code manually?

Angry rant: maybe mypy (and its PEPs) can be designed well? Maybe tacking java on top of python was a terrible idea, and python is much better than this awful type system.

cf. the syntactical catastrophe that is "protocols". Consider that to type `+` correctly, you're writing >dozen lines of python.

This is mad, and the type system shouldnt have been designed by people this inexperienced with type systems.

Wait until you use math in OCaML.

I quite enjoyed programming in OCaml.

Same, but the math system is strongly typed and doesn't have what the parent is talking about. There's more than one way to type a math system.

Python always had a type system. It's not checked ahead of time but it's there.

You can do things like return different types based on values read from a text file at runtime, that is it's a dependent type system. Python is not a total language - no termination proof of given functions to be found. It's also not pure, the calculation that picked a type can pick a different one next time it runs on the same arguments.

A dependent type system in a pure language with no user provided termination proof is in the ballpark of academia hasn't made it work yet.

Python's dynamic type system _cannot_ be checked at compile time, however much care goes into the design. What can be done is cripple python to some subset that can be statically typed, combining the elegance of java with the performance of python, with some end goal that doesn't make any sense to me.

This definition of dependent type system is a bit controversial. There was a conflict between Julia language maintainers and FP researchers a few years back.

Well, sort of. There's the (dominant?) school of thought that believes that types encode a program that runs before your actual program runs (and may thus be deleted at some point). This is often characterized by writing the type in a more awkward language than the usual one, C++'s separate languages for example.

Dependent Type Theory is quite strongly associated with the compiletime/runtime phase separation assumption, where the weirdness is that values from the runtime world leak into the compiletime one. This is magic in the static/AoT type world and trivial in the dynamic/JIT one.

So, strictly you're right, python is not dependently typed, as that term is owned by a different branch. However if you were to put an ahead of time type system on arbitrary python, that would need to be dependently typed to be able to describe the programs people write in python today. It would also be prone to failing to terminate during type checking.

Just make types functions which are executed at compile time:

    @type
    def Monoid(T: type):
        return {'+': type[T, T].to(T) }

    def add(left: Monoid(int), right: Monoid(int)): Monoid(int)
        return left + right

...if it takes too long to compile, terminate and report an error.

As for this kind of dependence, that seems straightforward:

    @type
    def Dependent():
       return {0: int, 1: str, "Hello": bool}

    def rtn_dependent(x: Dependent().keys): Dependent().values
      if x == 0: 
        return x
      elif x == 1:
        return "message"
      else:
        return x == "Hello"

Do you know of a type checking algorithm which is likely to deal with something like the second case? I'd say it would need to decompose the function body into cases and typecheck them individually - I think typed racket called the pattern occurance typing.

Push it a little harder though and you're into the domain of automatic theorem provers. Which is indeed an answer to how to write a dynamically typed program that doesn't need manual proof annotation - a great trick to have, but not one that exists yet as far as I know.

For what it's worth I quite like abort and apologize for a type check that takes too long. The termination requirement is probably flexible in practice.

I dont, but as far as practical compilation for python goes, i'm fairly happy with a type system that panics -- we dont need proofs, we need to model the underlying lang in a way 95% close to its actual semantics

For me, above, we can observe that all functions either return or implicitly return None. Therein lies a straightforward alg: are the types of all the returns consistent with the keys of the specified dict? etc. etc.

You may, for sure, need to run compile-time user-supplied fns to augemtn the type system. That's fine.

You can even, if needed, call run-time fns with generic args -- in order to determine their type.

"static" analysis need not presume the absense of a runtime.. only not a particular state of the runtime

Not actually sufficient though, you'll need:

def slow_add_int_float(a: int, b: float) -> float: # etc

where an argument could be made for encoding the return type in the name as well, at least for functions that don't do addition.

What that has going for it is the warm familiarity of C99. People really like function (and sometimes operator, if they draw a distinction) overloading though, and can reasonably argue that writing template instantiations by hand is a poor use of their time.

you should never be adding an int to a float. You should be casting one first.

Reply on news.ycombinator.com