Traditionally type systems are defined and then proved to be sound with respect to some well chosen semantics. We argue that the definition of the systems should come from their semantics and not the opposite. We use constrained type systems to define necessary conditions for types to be descriptions of terms. We then prove the soundness with respect to those conditions of the Curry and ML type systems.

Keywords: Type systems; Semantics of programming languages