4 ms·

You're actually missing the benefit of this. It's actually a feature. With python, because types are part of python itself, they can thus be programmable. You

You're actually missing the benefit of this. It's actually a feature. With python, because types are part of python itself, they can thus be programmable. You can create a function that takes in a typehint and returns a new typehint. This is legal python. For example below I create a function that dynamically returns a type that restricts a Dictionary to have a specific key and value. from typing import TypedDict def make_typed_dict(name: str, required_key: str, value_type: type): return TypedDict(name, {required_key: value_type, id: int}) # Example UserDict = make_typed_dict("UserDict", "username", str) def foo(data: UserDict): print(data["username"]) With this power in theory you can create programs where types essentially can "prove" your program correct, and in theory eliminate unit tests. Languages like idris specialize in this. But it's not just rare/specialized languages that do this. Typescript, believe it or not, has programmable types that are so powerful that writing functions that return types like the one above are Actually VERY common place. I was a bit late to the game to typescript but I was shocked to see that it was taking cutting edge stuff from the typing world and making it popular among users. In practice, using types to prove programs to be valid in place of testing is actually a bit too tedious compared with tests so people don't go overboard with it. It is a much more safer route then testing, but much harder. Additionally as of now, the thing with python is that it really depends on how powerful the typechecker is on whether or not it can enforce and execute type level functions. It's certainly possible, it's just nobody has done it yet. I'd go further than this actually. Python is actually a potentially more powerfully typed language than TS. In TS, types are basically another language tacked onto javascript. Both languages are totally different and the typing language is very very limited. The thing with python is that the types and the language ARE the SAME thing. They live in the same universe. You complained about this, but there's a lot of power in that because basically types become turing complete and you can create a type that does anything including proving your whole program correct. Like I said that power depends on the typechecker. Someone needs to create a typechecker that can recognize type level functions and so far it hasn't happened yet. But if you want to play with a language that does this, I believe that language is Idris.

quietbritishjim 1y ago
That's not a benefit. That's a monstrosity. And, as you heavily imply in your post, type checkers won't be able to cope with it, eliminating one if the main benefits of type hints. Neither will IDEs / language servers, eliminating the other main benefit.
- ninetyninenine 1y ago
  >And, as you heavily imply in your post, type checkers won't be able to cope with it I implied no such thing. literally said there's a language that already does this. Typescript. IDE's cope with it just fine. >That's not a benefit. That's a monstrosity. So typescript is a monstrosity? Is that why most of the world who uses JS in node or the frontend has moved to TS? Think about it.
  - baobun 1y ago
    I don't believe Typescript (nor Idris) type systems work like you describe, though? Types aren't programmable with code like that (in the same universe, as you say) and TS is structurally typed, with type erasure (ie types are not available at runtime). I am not that deeply familiar with Python typings development but it sounds fundamentally different to the languages you compare to.
    - ninetyninenine 1y ago
      Typescript types (and Idris) are Turing complete. You can actually get typescript types to run doom. https://www.youtube.com/watch?v=0mCsluv5FXA&t https://www.youtube.com/watch?v=0mCsluv5FXA&t Idris on the other hand is SPECIFICALLY designed so types and the program live in the same language. See the documentation intro: https://www.idris-lang.org/pages/example.html https://www.idris-lang.org/pages/example.html THe powerful thing about these languages is that they can prove your program correct. For testing you can never verify your program to be correct. Testing is a statistical sampling technique. To verify a program as correct via tests you have to test every possible input and output combination of your program, which is impractical. So instead people write tests for a subset of the possibilities which ONLY verifies the program as correct for that subset. Think about it. If you have a function: def add(x: int, y: int) -> int How would you verify this program is 100% correct? You have to test every possible combination of x, y and add(x, y). But instead you test like 3 or 4 possibilities in your unit tests and this helps with the overall safety of the program because of statistical sampling. If a small sample of the logic is correct, it says something about the entire population of the logic.. Types on the other hand prove your program correct. def add(x: int, y: int) -> int: return x + y If the above is type checked, your program is proven correct for ALL possible types. If those types are made more advanced via being programmable, then it becomes possible for type checking to prove your ENTIRE program correct. Imagine: def add<A: addable < 4, B: addable < 4>(x: A, y: B) -> A + B: return x + y With a type checker that can analyze the above you can create a add function that at most can take an int that is < 4 and return an int that is < 8. Thereby verifying even more correctness of your addition function. Python on the other hand doesn't really have type checking. It has type hints. Those type hints can de defined in the same language space as python. So a type checker must read python to a limited extent in order to get the types. Python at the same time can also read those same types. It's just that python doesn't do any type checking with the types while the type checker doesn't do anything with the python code other than typecheck it. Right now though, for most typecheckers, if you create a function in python that returns a typehint, the typechecker is not powerful enough to execute that function to find the final type. But this can certainly be done if there was a will because Idris has already done this.

quietbritishjim 1y ago

That's not a benefit. That's a monstrosity. And, as you heavily imply in your post, type checkers won't be able to cope with it, eliminating one if the main benefits of type hints. Neither will IDEs / language servers, eliminating the other main benefit.

ninetyninenine 1y ago
>And, as you heavily imply in your post, type checkers won't be able to cope with it I implied no such thing. literally said there's a language that already does this. Typescript. IDE's cope with it just fine. >That's not a benefit. That's a monstrosity. So typescript is a monstrosity? Is that why most of the world who uses JS in node or the frontend has moved to TS? Think about it.
- baobun 1y ago
  I don't believe Typescript (nor Idris) type systems work like you describe, though? Types aren't programmable with code like that (in the same universe, as you say) and TS is structurally typed, with type erasure (ie types are not available at runtime). I am not that deeply familiar with Python typings development but it sounds fundamentally different to the languages you compare to.
  - ninetyninenine 1y ago
    Typescript types (and Idris) are Turing complete. You can actually get typescript types to run doom. https://www.youtube.com/watch?v=0mCsluv5FXA&t https://www.youtube.com/watch?v=0mCsluv5FXA&t Idris on the other hand is SPECIFICALLY designed so types and the program live in the same language. See the documentation intro: https://www.idris-lang.org/pages/example.html https://www.idris-lang.org/pages/example.html THe powerful thing about these languages is that they can prove your program correct. For testing you can never verify your program to be correct. Testing is a statistical sampling technique. To verify a program as correct via tests you have to test every possible input and output combination of your program, which is impractical. So instead people write tests for a subset of the possibilities which ONLY verifies the program as correct for that subset. Think about it. If you have a function: def add(x: int, y: int) -> int How would you verify this program is 100% correct? You have to test every possible combination of x, y and add(x, y). But instead you test like 3 or 4 possibilities in your unit tests and this helps with the overall safety of the program because of statistical sampling. If a small sample of the logic is correct, it says something about the entire population of the logic.. Types on the other hand prove your program correct. def add(x: int, y: int) -> int: return x + y If the above is type checked, your program is proven correct for ALL possible types. If those types are made more advanced via being programmable, then it becomes possible for type checking to prove your ENTIRE program correct. Imagine: def add<A: addable < 4, B: addable < 4>(x: A, y: B) -> A + B: return x + y With a type checker that can analyze the above you can create a add function that at most can take an int that is < 4 and return an int that is < 8. Thereby verifying even more correctness of your addition function. Python on the other hand doesn't really have type checking. It has type hints. Those type hints can de defined in the same language space as python. So a type checker must read python to a limited extent in order to get the types. Python at the same time can also read those same types. It's just that python doesn't do any type checking with the types while the type checker doesn't do anything with the python code other than typecheck it. Right now though, for most typecheckers, if you create a function in python that returns a typehint, the typechecker is not powerful enough to execute that function to find the final type. But this can certainly be done if there was a will because Idris has already done this.