11 Nov 00:39 1987

### Re: Type : Type

Dear Uday, Thanks for your question. What is common to "TYPE : TYPE" and "TRIV :: TRIV" is (one of) the intuitions that they both capture. I have assumed that it is of interest, at least for programming languages, to capture the intuition that that "T : TYPE" means "T defines some structure", using an approach that does(Continue reading)*not*require making sense of anything like things being members of themselves, but that still allows (its version of) "TYPE : TYPE" to mean that "TYPE defines some structure". Part of what makes our approach workable is that models also appear as types (i.e., as theories). Thus, NAT :: TRIV technically means that the _theory of natural numbers_*satisfies*TRIV,*not*that some particular model of NAT, say omega, is a*member*of TRIV, though of course its intuition is that omega is a member of (the*denotation*of) TRIV. A nice fringe benefit of this approach is that*abstractness*is automatic: the denotation of NAT is actually the _abstract data type_ for the natural numbers, i.e., the (category of) algebras that satisfy NAT, which is the category of algebras*isomorphic*to omega; in fact, omega plays no privileged role here at all. (Data constraints provide the underlying machinery giving theories that impose initiality on models.) Going a little further down this route, the denotation of the theory interpretation TRIV -> NAT (which is the actual content of "NAT :: TRIV") is the forgetful functor which gives the underlying sets of these algebras.