Phase Distinction is a property of programming languages that observe a strict division between types and terms. A concise rule for determining whether phase distinction is preserved in a language or not has been proposed by Luca Cardelli - If A is a compile-time term and B is a subterm of A, then B must also be a compile-time term. A language with phase distinction may have separate namespaces for types and run-time variables. In an optimizing compiler, phase distinction marks the boundary between expressions which are safe to erase.