Search

Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped $\lambda$-abstractions (i.e. of the form $\lambda{x}.{M}$); and domain-free systems with typed $\lambda$-abstractions (i.e. of the form $\lambda{x}{A}{M}$). Both flavours of systems are related by an erasure function $\er{.}$ that removes types from $\lambda$-abstractions. Preservation of Equational Theory, which states the equational theories of both systems coincide through the erasure function, is a property of functional and normalizing PTSs. In this paper we establish that Preservation of Equational Theory fails for some non-normalizing PTSs, including the PTS with $\ast:\ast$. The gist of our argument is to exhibit a typable expression $Y_H$ whose erasure $\er{Y}$ is a fixpoint combinator, but which is not a fixpoint combinator itself. [ABSTRACT FROM AUTHOR]

Modern programming languages rely on advanced type systems that detect errors at compile-time. While the benefits of type systems have long been recognized, there are some areas where the standard systems in programming languages are not expressive enough. Language designers usually trade expressiveness for decidability of the type system. Some interesting programs will always be rejected (despite their semantical soundness) or be assigned uninformative types. [ABSTRACT FROM AUTHOR]