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

universe elimination rules (replies)


|| Thanks to Robert and Thorsten

|| Robert Harper's reply

At 9:31 AM 8/22/95, Daniel Mahler wrote:
>Could someone tell me what are universe elimination rules in type theories.
>
>Do they have something to do with quantifying or abstracting over universes?
>Are there type systems which actually do this?
>
>        thanks
>        Daniel Mahler
>
>[All, Please send your replies to Daniel Mahler.
> Daniel Mahler, Please summarise your replies to the Types Forum.
>  -- Philip Wadler, moderator, Types Forum.]

I'm sure there must be many variants of this idea.  Back in the early 80's
we experimented with universe elimination in the NuPRL system.  Roughly
speaking, a "universe" is a type of types (or, in some versions, a type of
"names" for types).  Of course the universe does not contain ALL types; in
particular, the universe itself is not a type contained in the universe.
In the simplest formulation universes are considered to be open-ended: we
specify a collection of things that ARE in the universe, without requiring
that these be the ONLY inhabitants.  The idea of a universe elimination
rule (in the sense explored with NuPRL) is to think of universes as
inductively generated, with a structural induction principle as elimination
form.  This allows you to define functions over a universe by analyzing the
structure of its members.  This proposal never made it into the "official"
definition of NuPRL, though, so I don't believe it is written down anywhere
in the NuPRL literature.

More recently Greg Morrisett and I revived this idea in connection with
compiling polymorphic languages.  See our paper in the last POPL entitled
"Compiling Polymorphism Using Intensional Type Analysis".  Using universe
elimination we are able to compile ML much more efficiently than was
previously possible (in many cases), and to extend the expressiveness of
the language considerably.

Bob Harper

|| Thorsten Altenkirch's reply

>>>>> "Daniel" == Daniel Mahler <mahler@socs.uts.EDU.AU> writes:

    Daniel> Could someone tell me what are universe elimination rules
    Daniel> in type theories.

Universes can be viewed as a (generalized) case of inductive
definitions or as Peter Dybjer calls them "inductive-recursive"
definitions. Elimination rules (aka non-canonical constants) for
universes hence play the same role as the elimination rules for other
inductive definitions (e.g. induction or primitive recursion for
natural numbers). They express that all the canonical elements of the
universes are generated by a finite application of the constructors.

As a simple example a universe with pi-types and natural numbers is
defined as follows (assuming that we have set formers Nat and Pi)

Formation

	U : Set
	T : U -> Set

Intros

	nat : U
	pi : (A:U;B:T(A)->U)U

Equalities

	T(nat) = Nat
	T(pi(A,B)) = Pi(a:T(A),T(B(a)))

So T is a non-canonical constant (e.g. corresponding to an elimination
rule). The special thing about universes is that T is defined
mutually with the constructors, hence "inductive-recursive"
definitions.

In the ALF system (which is an implementation of a varaint of
Martin-L"of Type Theory form Goeteborg) we usually do not define a
standard elimination rule but allow the additition of non-canonical
constants which are defined by structural recursion and pattern
matching (following a proposal of Thierry Coquand). However, you can
also define a "standard" elimination rule for universes:

	U_rec : (P:U->Set;
		 P(nat);
	         (A:U;P(A);B:T(A)->U;(a:T(A))P(B(a)))P(pi(A,B);
		 A:U)P(A)                 

	U_rec (P,n,p,nat) = n
	U_rec (P,n,p,pi(A,B)) = 
		p(A,U_rec(P,n,p,A),B,[a]U_rec(P,n,p,B(a)))

    Daniel> Do they have something to do with quantifying or
    Daniel> abstracting over universes?  Are there type systems which
    Daniel> actually do this?

I will try to give you an example although this doesn't use the
standard universe but a similar construction. If you want to do a
normalization proof for simply typed lambda calculus ala
Tait,Girard,... you will define the syntax of types and their
interpretation by a universe like constructionm e.g. assume we have
Tm:Set (the set of lambda terms) with a constructor app: (Tm;Tm)Tm and
SN : Tm->Set the predicate "strongly normalizing" then we define

	U : Set
	T : U -> (Tm -> Set)

	o : U
	arr : (U;U)U

	T(o) = SN
	T(arr(A,B)) = [t](u:Tm)T(A)(u) -> T(B)(app(t,u))

An application for the general universe elimination would be the proof
that the interpretation of all types are candidates in sense of Girard
(or saturated sets), e.g. assume a predicate CR: (Tm->Set)->Set

	CR_lem : (A:U)CR(T(A))

which plays an important role in the proof.

You may remark that the example above is degenerate in the sense that
U and T do not depend on each other mutually. This is related to the
fact that we only show normalization for a non-dependent theory. A
normalization proof for a calculus with dependent types might use a
univers of the more general form. However, encoding the syntax of
dependent types is technically tricky.

-- 
Thorsten Altenkirch	(alti@cs.chalmers.se)
Computer Science, Chalmers University of Technology, Sweden
DISCLAIMER: All opinions expressed here are my own.
WWW URL: http://www.cs.chalmers.se/~alti