The claim that the concept of "type" is not formally defined, is rather like saying that the concept of "logic" is not formally defined. In both cases there are several competing, completely formal definitions, each with their own scope and uses.
If one is really serious about studying types one should read some of Per Martin-Löf's more philosophical writings on the topic. In his dependent type theory there is a clear extensible philosophical notion of what constitutes a type (being defined by its introduction rules) — and a clear computational meaning.
The fact that one needs concepts like monads to describe effectful programs is not really more surprising than the fact that one needs the concept of a mathematical manifold to describe certain parts of physics. The cool thing is that these mathematical descriptions of effect can actually be used to do effectful programming, thanks to the computational nature of types.
Type has a formal definition for sure, but it is quite different from its more accepted informal definition. There are also those who study types for the sake of types and those who are more interested in type systems for the sake of building programming languages...these are increasingly very different fields.
If one is really serious about studying types one should read some of Per Martin-Löf's more philosophical writings on the topic. In his dependent type theory there is a clear extensible philosophical notion of what constitutes a type (being defined by its introduction rules) — and a clear computational meaning.
The fact that one needs concepts like monads to describe effectful programs is not really more surprising than the fact that one needs the concept of a mathematical manifold to describe certain parts of physics. The cool thing is that these mathematical descriptions of effect can actually be used to do effectful programming, thanks to the computational nature of types.