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.
>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.
The syntax is a monstrosity. You can also extract a proven OCaml program from Coq and Coq has a beautiful syntax.
If you insist on the same language for specifying types, some Lisp variants do that with a much nicer syntax.
Python people have been indoctrinated since ctypes that a monstrous type syntax is normal and they reject anything else. In fact Python type hints are basically stuck on the ctypes level syntax wise.
That's just a sugar thing. Yeah it can get a bit more verbose.
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.
Typescript types (and Idris) are Turing complete. You can actually get typescript types to run doom.
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
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:
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.
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:
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.