Pure Type Systems for Functional Programming

We present a functional programming language based on Pure Type Systems PTSs. We show how we can define such a language by extending the PTS framework with algebraic data types case expressions and definitions. Furthermore we present an efficient type checking algorithm and an interpreter for this language. PTSs are well suited as a basis for a functional programming language because they are at the top of a hierarchy of increasingly stronger type systems. The concepts of existential types rank-n polymorphism and dependent types arise naturally in functional programming languages based on the systems in this hierarchy. There is no need for ad-hoc extensions to incorporate these features. The type system of our language is more powerful than the Hindley Milner system We illustrate this fact by giving a number of meaningful programs that cannot be typed in Haskell but are typable in our language