> because we don't have to type type definitions
Typing "type definitions" makes you type less, not more, because you type the definition only once, instead of writing many tests wherever values of that type are used.
In a decent programming language, one would frequently avoid the need to declare the type of a variable, whenever the type can be deduced from the value used to initialize the variable.
Having types in a language has 2 purposes, one is to enable the compiler to check at compile time or at run type that all the subsequent uses of an identifier after its first occurrence are consistent.
I cannot imagine which are the benefits for the programmers who are against this rule, i.e. who want to reuse the same identifier for multiple purposes in the same scope (N.B. reusing an identifier in the same scope has nothing to do with data types that are disjoint unions or virtual types, which can be used in any type-enforcing language, or with reusing the same identifier in different scopes).
The second purpose of data types is that when the type of a variable or parameter is known at compile-time, that allows more efficient implementations, which are especially important for aggregated data, e.g. arrays.
Again, I also do not understand why anyone would want to have inefficient data representations, to avoid the need of data types.
There has been some argument that when a language does not use data types you might avoid having to rewrite some library functions if you want to change the parameter types at invocation. However this is a problem that has been better solved for more than a half of century, by providing various means to write generic functions that can be specialized at compile-time or by using disjoint union types or virtual types, for using the same function for many different data types, while still ensuring that other data types, whose use would be erroneous, are rejected.
A language without data types saves writing effort only when the programmer omits the run-type checks for correct values, which would be needed to avoid bugs when such checks are not done automatically by the compiler.
I agree that several very popular programming languages with type checking, including C and C++, are very poor examples about how a type system should be implemented, because they require the writing of a great amount of superfluous boilerplate that is completely unnecessary (e.g. writing headers with function declarations instead of extracting automatically the interfaces of a package a.k.a. module or writing explicit type names in a lot of places where they can be deduced automatically from the context).
Such languages are strawmen in a discussion about whether a language must enforce type checking or not.