As a thought experiment, I like to assume that there is a hypothetical language where everything is encoded in types, to the point where you don't have or need

As a thought experiment, I like to assume that there is a hypothetical language where everything is encoded in types, to the point where you don't have or need variable names anymore. Every typed language (and programming style) we use is some point in the spectrum of practical compromises between that hypothetical language where all pre-runtime information is in formal types and scripting languages where all pre-runtime information is in informal names. Java for example has to leave quite a lot of that information in names because there are no type aliases and final types exist.