"Type" is not a type

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.

REFERENCES

• 1: Reference manual for the Ada programming language. G.P.O. 008-000-00354-8, 1980.
• 2: H. P. Barendregt. <i>The Lambda Calculus: Its Syntax and Semantics.</i> Volume 103 of <i>Studies in Logic and the Foundations of Mathematics,</i> North-Holland, Amsterdam, second edition, 1984.
• 3: Henk Barendregt , Adrian Rezus, Semantics for classical AUTOMATH and related systems, Information and Control, v.59 n.1-3, p.127-147, Oct./Nov./Dec. 1983 [doi>10.1016/S0019-9958(83)80033-3]
• 4: Hans Boehm , Alan J. Demers , James E. Donahue, An Informal Description of Russell, Cornell University, Ithaca, NY, 1980
• 5: Kim B. Bruce , Albert R. Meyer, The semantics of second order polymorphic lambda calculus., Proc. of the international symposium on Semantics of data types, p.131-156, July 1984, Sophia-Antipolis, France
• 6: R. Burstall , B. Lampson, A kernel language for abstract data types and modules., Proc. of the international symposium on Semantics of data types, p.1-50, July 1984, Sophia-Antipolis, France
• 7: Thierry Coquand , Gérard P. Huet, Constructions: A Higher Order Proof System for Mechanizing Mathematics, Invited Lectures from the European Conference on Computer Algebra-Volume I, p.151-184, April 01-03, 1985
• 8: H. B. Curry and R. Feys. <i>Combinatory Logic.</i> Volume 1, North-Holland, Amsterdam, 1958.
• 9: N. G. de Bruijn. Lambda-calculus notation with nameless dummies. <i>Indag. Math.,</i> 34(5):381--392, 1972.
• 10: N. G. de Bruijn. A survey of the project AUTOMATH. In J. P. Seldin and R. Hindley, editors, <i>To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism,</i> pages 579--606, Academic Press, New York, 1980.
• 11: James Donahue , Alan Demers, Data types are values, ACM Transactions on Programming Languages and Systems (TOPLAS), v.7 n.3, p.426-445, July 1985 [doi>10.1145/3916.3987]
• 12: Steven Fortune , Daniel Leivant , Michael O'Donnell, The Expressiveness of Simple and Second-Order Type Structures, Journal of the ACM (JACM), v.30 n.1, p.151-185, Jan. 1983 [doi>10.1145/322358.322370]
• 13: G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, <i>The Collected Papers of Gerhard Gentzen,</i> North-Holland, Amsterdam, 1969.
• 14: G. Gentzen. Investigations into logical deduction. <i>Mathematische Zeitschrift,</i> 39:176--210 and 405--431, 1934. See {13} for an English translation.
• 15: J. Girard. <i>Interpr&eacute;tation fonctionelle et &eacute;limination des coupures dans l'arithm&eacute;tique d'ordre sup&eacute;ricure.</i> Ph.D. thesis, Universit&eacute; Paris VII, 1972.
• 16: W. A. Howard. The formulae-as-types notion of construction. 1969. Recently published as {17}.
• 17: W. A. Howard. The formulae-as-types notion of construction. In J. P. Seldin and R. Hindley, editors, <i>To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism,</i> pages 479--490, Academic Press, New York, 1980.
• 18: B Liskov , E Moss , A Snyder , R Atkinson , J C. Schaffert , T Bloom , R Scheifler, CLU reference manual, Springer-Verlag New York, Inc., New York, NY, 1984
• 19: P. Martin-L&ouml;f. An intuitionistic theory of types: predicative part. In F. Rose and J. Sheperdson, editors, <i>Logic Colloquium III,</i> pages 73--118, North-Holland, Amsterdam, July 1973.
• 20: P. Martin-L&ouml;f. <i>A Theory of Types.</i> Report 71--3, Department of Mathematics, University of Stockholm, February 1971.
• 21: Nancy Jean Mccracken, An investigation of a programming language with a polymorphic type structure., 1979
• 22: John C. Mitchell , Albert R. Meyer, Second-Order Logical Relations (Extended Abstract), Proceedings of the Conference on Logic of Programs, p.225-236, June 17-19, 1985
• 23: J. C. Mitchell. <i>Lambda Calculus Models of Typed Programming Languages.</i> Ph.D. thesis, Massachusetts Institute of Technology, Cambridge, Massachusetts, August 1984.
• 24: John C. Mitchell , Gordon D. Plotkin, Abstract types have existential types, Proceedings of the 12th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.37-51, January 14-16, 1985, New Orleans, Louisiana, United States [doi>10.1145/318593.318606]
• 25: Lawrence Paulson, Deriving structural induction in LCF., Proc. of the international symposium on Semantics of data types, p.197-214, July 1984, Sophia-Antipolis, France
• 26: G. D. Plotkin. Personal communication, March 1985.
• 27: D. Prawitz. <i>Natural Deduction: A Proof-Theoretical Study.</i> Volume 3 of <i>Stockholm Studies in Philosophy,</i> Almqvist and Wiksell, Stockholm, 1965.
• 28: J. C. Reynolds. Polymorphism is not set-theoretic. In G. Kahn, D. B. MacQueen, and G. D. Plotkin, editors, <i>Semantics of Data Types,</i> pages 145--156, Springer-Verlag, Berlin, June 1984.
• 29: John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
• 30: J. C. Reynolds. Types, abstraction, and parametric polymorphism. In R. E. A. Mason, editor, <i>Information Processing 83,</i> pages 513--523, North-Holland, 1983.
• 31: A. Rezus. <i>Abstract AUTOMATH.</i> Mathematical Centre Tract 160, Mathematisch Centrum, Amsterdam, 1983.