[Prev][Next][Index][Thread]

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
*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.

The use of theory interpretations seems to allow a significant extension of
the notion of something having a type.  For there are many cases where you
must either admit more than one way for something to have a type, or else say
that there is no way.  For example,

	NAT : MONOID

is ambiguous, assuming that NAT has been defined with both addition and
multiplicaton, since there are two distinct theory morphisms MONOID -> NAT.
(In our languages OBJ, etc., convention determines one of these as the meaning
of the default syntax; you can still get the other by being explicit.)

I hope that this makes things a little clearer.

Cheers,

Joseph
--------