| ▲ | copx 2 hours ago | |
Probably not. Most popular programming languages have messy - unsound and/or undecidable - type systems e.g. C++, C#, TypeScript, Java,.. ..because that is more practical. | ||
| ▲ | epolanski 18 minutes ago | parent | next [-] | |
Can you make an example of TypeScript's unsoundness that cannot be fixed with better encodings? | ||
| ▲ | js8 42 minutes ago | parent | prev [-] | |
I don't think it's more practical, being able to do things like type inference on return value is actually really cool. Maybe more practical for the programming language developer (less learning about type systems) than for the user.. but then you have to ask why build another language? | ||