Quotient Types: A Modular Approach.

Aleksey Nogin
Quotient Types: A Modular Approach.
In Victor A. Carreño, Cézar A. Muñoz, and Sophiène Tahar, editors, Proceedings of the 15th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2002), volume 2410 of Lecture Notes in Computer Science, pages 281--297. Springer-Verlag, 2002.
LNCS Entry, PDF (271KB), PS (886 KB)

Earlier version:
Aleksey Nogin
Quotient Types — a Modular Approach.
Department of Computer Science TR2002-1869, Cornell University, April 2002
Cornell Tech Reports Entry, PDF (304KB), PostScript (245KB)

Abstract

In this paper we introduce a new approach to axiomatizing quotient types in type theory. We suggest replacing the existing monolithic rule set by a modular set of rules for a specially chosen set of primitive operations. This modular formalization of quotient types turns out to be much easier to use and free of many limitations of the traditional monolithic formalization. To illustrate the advantages of the new approach, we show how the type of collections (that is known to be very hard to formalize using traditional quotient types) can be naturally formalized using the new primitives. We also show how modularity allows us to reuse one of the new primitives to simplify and enhance the rules for the set types.