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"])
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.
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.
That's horrible. Nobody needs imperative metaprogramming for type hints. In fact, it would be absolute insanity for a typechecker to check this because it would mean opening a file in VS code = executing arbitrary python code. What stops me from deleting $HOME inside make_typed_dict?
TypeScript solves this with its own syntax that never gets executed by an interpreter because types are striped when TS is compiled to JS.
>VS code = executing arbitrary python code. What stops me from deleting $HOME inside make_typed_dict?
Easy make IO calls illegal in the type checker. The type checker of course needs to execute code in a sandbox. It won't be the full python language. Idris ALREADY does this.
Are there really productive projects which rely on types as a proofing system? I've always thought it added too much complexity to the code, but I'd love to see it working well somewhere. I love the idea of correctness by design.
No too my knowledge nothing is strict about a proofing system because like I said it becomes hard to do. It could be useful for ultra safe software but for most cases the complexity isn't worth it.
But that doesn't mean it's not useful to have this capability as part of your typesystem. It just doesn't need to be fully utilized.
You don't need to program a type that proves everything correct. You can program and make sure aspects of the program are MORE correct than just plain old types. typescript is a language that does this and it is very common to find types in typescript that are more "proofy" than regular types in other languages.
See here: https://www.hacklewayne.com/dependent-types-in-typescript-se...
Typescript does this. Above there's a type that's only a couple of lines long that proves a string reversal function reverses a string. I think even going that deep is overkill but you can define things like Objects that must contain a key of a specific string where the value is either a string or a number. And then you can create a function that dynamically specifies the value of the key in TS.
I think TS is a good example of a language that practically uses proof based types. The syntax is terrible enough that it prevents people from going overboard with it and the result is the most practical application of proof based typing that I seen. What typescript tells us that proof based typing need only be sprinkled throughout your code, it shouldn't take it all over.