This paper, presented at the Colloquium on Programming in Paris in 1974, by John C. Reynolds from Syracuse University, explores the principles of type structure in programming languages. The author formalizes a view similar to that of J. H. Morris, introducing an extension of the typed lambda calculus that supports user-defined types and polymorphic functions. The semantics of this language is shown to satisfy a representation theorem, which ensures that the meaning of a syntactically valid program should not depend on the specific representations used for its primitive types. The paper begins by discussing the importance of representation independence, where the meaning of a program should remain unchanged if the representation of a type is altered. This concept is extended to user-defined types, where the inner region of a program, which defines the representation of a type, can be changed without affecting the program's meaning. The introduction of polymorphic functions, originally posed by Strachey, is also addressed. The paper 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 include type variables and polymorphic functions. The syntax and semantics of this language are formally defined, including the use of type expressions and normal expressions. The semantics are interpreted using a lattice-theoretic approach, where type expressions produce Scott domains given assignments of domains to type variables. The paper concludes with a representation theorem that formalizes the idea that the meaning of a program should be independent of the representations used for its types. The theorem is proved using category theory, defining functors and morphisms to extend the semantic function from domains to representations. The paper also discusses some syntactic manipulations and open questions, particularly regarding the completeness of the language's normal forms.This paper, presented at the Colloquium on Programming in Paris in 1974, by John C. Reynolds from Syracuse University, explores the principles of type structure in programming languages. The author formalizes a view similar to that of J. H. Morris, introducing an extension of the typed lambda calculus that supports user-defined types and polymorphic functions. The semantics of this language is shown to satisfy a representation theorem, which ensures that the meaning of a syntactically valid program should not depend on the specific representations used for its primitive types. The paper begins by discussing the importance of representation independence, where the meaning of a program should remain unchanged if the representation of a type is altered. This concept is extended to user-defined types, where the inner region of a program, which defines the representation of a type, can be changed without affecting the program's meaning. The introduction of polymorphic functions, originally posed by Strachey, is also addressed. The paper 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 include type variables and polymorphic functions. The syntax and semantics of this language are formally defined, including the use of type expressions and normal expressions. The semantics are interpreted using a lattice-theoretic approach, where type expressions produce Scott domains given assignments of domains to type variables. The paper concludes with a representation theorem that formalizes the idea that the meaning of a program should be independent of the representations used for its types. The theorem is proved using category theory, defining functors and morphisms to extend the semantic function from domains to representations. The paper also discusses some syntactic manipulations and open questions, particularly regarding the completeness of the language's normal forms.