In academia, "type theory" almost always means dependent type theory, such as Martin-Löf type theory or homotopy type theory. Type theory is used in most theorem provers as a foundation for mathematics. The title of this blog post is using the term in a standard way.
Programming languages such as Haskell and Java are not based on type theory. They have type systems. Haskell's type system is much closer to type theory than that of Java, but it's still quite crippled compared to what type theorists study.
It is of course possible to define things in type theory such that 1/0 = Infinity or something else, but that is not the norm.
Programming languages such as Haskell and Java are not based on type theory. They have type systems. Haskell's type system is much closer to type theory than that of Java, but it's still quite crippled compared to what type theorists study.
It is of course possible to define things in type theory such that 1/0 = Infinity or something else, but that is not the norm.