Polymorphism and Information Loss in Martin-Loef's Type Theory

摘要

A type of polymorphic object is examined and it is shown how this type allows the derivation of concise programs in type theory. The head function on lists is presented as an example. The relationship between polymorphism and information loss is captured in some derived rules which allow inductive reasoning over restricted domains. An example is given of how these rules may be used in defining new data types such as balanced trees.