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:

    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.