This preprint presents a paper to be presented at the Colloquium on Programming in Paris, April 1974. The paper explores the theory of type structure in programming languages. John C. Reynolds introduces an extension of the typed lambda calculus that allows user-defined types and polymorphic functions. He argues that the semantics of this language satisfies a representation theorem that embodies a notion of "correct" type structure. The paper begins by stating that the meaning of a syntactically valid program in a "type-correct" language should not depend on the specific representations used for primitive types. It then discusses the concept of representation independence, where user-defined types should behave like primitive types in an outer region and be defined in terms of other types in an inner region. The meaning of the program should remain unchanged if the inner region is altered consistently. The paper also addresses the problem of polymorphic functions, which are functions that can operate on multiple types. Reynolds suggests that types themselves can be passed as parameters to allow syntactic checking of type correctness. An illustrative language is introduced, which extends the typed lambda calculus to allow binding of type variables. This language is used to formalize the semantics of type structures. The paper defines a function B that maps type expressions to domains, and a function M that maps normal expressions to values, ensuring type correctness. The paper then defines the concept of representation between domains and discusses the representation theorem, which asserts that the meaning of a program remains consistent under different representations. The theorem is formalized using category theory, with the category of types and functors between them. The paper concludes by discussing the semantics of type expressions and the properties of representations, leading to the proof of the representation theorem through structural induction. It also addresses some syntactic manipulations and the challenges in defining the representation theorem, including the issue of countable basis for certain structures. The paper acknowledges the contributions of Dr. Lockwood Morris.This preprint presents a paper to be presented at the Colloquium on Programming in Paris, April 1974. The paper explores the theory of type structure in programming languages. John C. Reynolds introduces an extension of the typed lambda calculus that allows user-defined types and polymorphic functions. He argues that the semantics of this language satisfies a representation theorem that embodies a notion of "correct" type structure. The paper begins by stating that the meaning of a syntactically valid program in a "type-correct" language should not depend on the specific representations used for primitive types. It then discusses the concept of representation independence, where user-defined types should behave like primitive types in an outer region and be defined in terms of other types in an inner region. The meaning of the program should remain unchanged if the inner region is altered consistently. The paper also addresses the problem of polymorphic functions, which are functions that can operate on multiple types. Reynolds suggests that types themselves can be passed as parameters to allow syntactic checking of type correctness. An illustrative language is introduced, which extends the typed lambda calculus to allow binding of type variables. This language is used to formalize the semantics of type structures. The paper defines a function B that maps type expressions to domains, and a function M that maps normal expressions to values, ensuring type correctness. The paper then defines the concept of representation between domains and discusses the representation theorem, which asserts that the meaning of a program remains consistent under different representations. The theorem is formalized using category theory, with the category of types and functors between them. The paper concludes by discussing the semantics of type expressions and the properties of representations, leading to the proof of the representation theorem through structural induction. It also addresses some syntactic manipulations and the challenges in defining the representation theorem, including the issue of countable basis for certain structures. The paper acknowledges the contributions of Dr. Lockwood Morris.