Albert R. Meyer
Mark B. Reinhold
ABSTRACT
A function has a <i>dependent type</i> when the type of its result depends upon the value of its argument. Dependent types originated in the type theory of intuitionistic mathematics and have reappeared independently in programming languages such as CLU, Pebble, and Russell. Some of these languages make the assumption that there exists a <i>type-of-all-types</i> which is its own type as well as the type of all other types. Girard proved that this approach is inconsistent from the perspective of intuitionistic logic. We apply Girard's techniques to establish that the type-of-all-types assumption creates serious pathologies from a programming perspective: a system using this assumption is inherently not normalizing, term equality is undecidable, and the resulting theory fails to be a conservative extension of the theory of the underlying base types. The failure of conservative extension means that classical reasoning about programs in such a system is not sound.
- Reference manual for the Ada programming language. G.P.O. 008-000-00354-8, 1980.Google Scholar
- H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Volume 103 of Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam, second edition, 1984.Google Scholar
- H. P. Barendregt and A. Rezus. Semantics for classical AUTOMATH and related systems. Information and Control, 59:127--147, 1983. Google ScholarDigital Library
- H. Boehm, A. Demers, and J. Donahue. An Informal Description of Russell. Technical Report TR80-430, Cornell University, Computer Science Department, 1980. Google ScholarDigital Library
- K. B. Bruce and A. R. Meyer. The semantics of second order polymorphic lambda calculus. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 131--144, Springer-Verlag, Berlin, June 1984. Google ScholarDigital Library
- R. Burstall and B. W. Lampson. A kernel language for abstract data types and modules. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 1--50, Springer-Verlag, Berlin, June 1984. Google ScholarDigital Library
- T. Coquand and G. Huet. Constructions: A Higher Order Proof System for Mechanizing Mathematics. Rapport de Recherche 401, INRIA, Domaine de Voluceau, 78150 Rocquencourt, France, May 1985. Presented at EUROCAL 85, Linz, Austria. Google ScholarDigital Library
- H. B. Curry and R. Feys. Combinatory Logic. Volume 1, North-Holland, Amsterdam, 1958.Google Scholar
- N. G. de Bruijn. Lambda-calculus notation with nameless dummies. Indag. Math., 34(5):381--392, 1972.Google ScholarCross Ref
- N. G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 579--606, Academic Press, New York, 1980.Google Scholar
- J. Donahue and A. Demers. Data types are values. ACM Transactions on Programming Languages and Systems, 7(3):426--445, July 1985. Google ScholarDigital Library
- S. Fortune, D. Leivant, and M. O'Donnell. The expressiveness of simple and second-order type structures. Journal of the ACM, 30(1):151--185, January 1983. Google ScholarDigital Library
- G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1969.Google Scholar
- G. Gentzen. Investigations into logical deduction. Mathematische Zeitschrift, 39:176--210 and 405--431, 1934. See {13} for an English translation.Google ScholarCross Ref
- J. Girard. Interpr&eacute;tation fonctionelle et &eacute;limination des coupures dans l'arithm&eacute;tique d'ordre sup&eacute;ricure. Ph.D. thesis, Universit&eacute; Paris VII, 1972.Google Scholar
- W. A. Howard. The formulae-as-types notion of construction. 1969. Recently published as {17}.Google Scholar
- W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and R. Hindley, editors, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pages 479--490, Academic Press, New York, 1980.Google Scholar
- B. Liskov, R. Atkinson, T. Bloom, E. Moss, J. C. Schaffert, R. Scheifler, and A. Snyder. CLU Reference Manual. Volume 114 of Lecture Notes in Computer Science, Springer-Verlag, Berlin, 1981. Google ScholarDigital Library
- P. Martin-L&ouml;f. An intuitionistic theory of types: predicative part. In F. Rose and J. Sheperdson, editors, Logic Colloquium III, pages 73--118, North-Holland, Amsterdam, July 1973.Google Scholar
- P. Martin-L&ouml;f. A Theory of Types. Report 71--3, Department of Mathematics, University of Stockholm, February 1971.Google Scholar
- N. J. McCracken. An Investigation of a Programming Language with a Polymorphic Type Structure. Ph.D. thesis, Syracuse University, Syracuse, New York, June 1979. Google ScholarDigital Library
- A. R. Meyer and J. C. Mitchell. Second-order logical relations (extended abstract). In R. Parikh, editor, Logics of Programs, pages 225--236, Springer-Verlag, Berlin, June 1985. Google ScholarDigital Library
- J. C. Mitchell. Lambda Calculus Models of Typed Programming Languages. Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts, August 1984.Google Scholar
- J. C. Mitchell and G. D. Plotkin. Abstract types have existential type. In Principles of Programming Languages, pages 37--51, ACM, New York, January 1985. Google ScholarDigital Library
- L. Paulson. Deriving structural induction in LCF. In G. Kahn, D. B. MacQueen, and G. Plotkin, editors, Semantics of Data Types, pages 197--214, Springer-Verlag, Berlin, June 1984. Google ScholarDigital Library
- G. D. Plotkin. Personal communication, March 1985.Google Scholar
- D. Prawitz. Natural Deduction: A Proof-Theoretical Study. Volume 3 of Stockholm Studies in Philosophy, Almqvist and Wiksell, Stockholm, 1965.Google Scholar
- J. C. Reynolds. Polymorphism is not set-theoretic. In G. Kahn, D. B. MacQueen, and G. D. Plotkin, editors, Semantics of Data Types, pages 145--156, Springer-Verlag, Berlin, June 1984.Google ScholarCross Ref
- J. C. Reynolds. Towards a theory of type structure. In B. Robinet, editor, Programming Symposium, pages 408--425, Springer-Verlag, Berlin, 1974. Google ScholarDigital Library
- J. C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, Information Processing 83, pages 513--523, North-Holland, 1983.Google Scholar
- A. Rezus. Abstract AUTOMATH. Mathematical Centre Tract 160, Mathematisch Centrum, Amsterdam, 1983.Google Scholar
- "Type" is not a type
Recommendations
Formalizing Type Operations Using the “Image” Type Constructor
In this paper we introduce a new approach to formalizing certain type operations in type theory. Traditionally, many type constructors in type theory are independently axiomatized and the correctness of these axioms is argued semantically. In this paper ...
Gradual type theory
Gradually typed languages are designed to support both dynamically typed and statically typed programming styles while preserving the benefits of each. While existing gradual type soundness theorems for these languages aim to show that type-based ...
Decidability of conversion for type theory in type theory
Type theory should be able to handle its own meta-theory, both to justify its foundational claims and to obtain a verified implementation. At the core of a type checker for intensional type theory lies an algorithm to check equality of types, or in ...
Comments