Cayenne—a language with dependent types

ABSTRACT

Cayenne is a Haskell-like language. The main difference between Haskell and Cayenne is that Cayenne has dependent types, i.e., the result type of a function may depend on the argument value, and types of record components (which can be types or values) may depend on other components. Cayenne also combines the syntactic categories for value expressions and type expressions; thus reducing the number of language concepts.Having dependent types and combined type and value expressions makes the language very powerful. It is powerful enough that a special module concept is unnecessary; ordinary records suffice. It is also powerful enough to encode predicate logic at the type level, allowing types to be used as specifications of programs. However, this power comes at a cost: type checking of Cayenne is undecidable. While this may appear to be a steep price to pay, it seems to work well in practice.

REFERENCES

• ACN90: L. Augustsson, T. Coquand, and B. NordstrSm. A short description of Another Logical Framework. In Proceedings of the First Workshop on Logical Frameworks, Antibes, pages 39-42, 1990.
• AJ89: L. Augustsson , T. Johnsson, The Chalmers lazy ML-compiler, The Computer Journal, v.32 n.2, p.127-141, April 1989 [doi>10.1093/comjnl/32.2.127]
• Aug93: Lennart Augustsson, Implementing Haskell overloading, Proceedings of the conference on Functional programming languages and computer architecture, p.65-73, June 09-11, 1993, Copenhagen, Denmark [doi>10.1145/165180.165191]
• BDD89: H. Boehm, A. Demers, and J. Donahue. A Programmer's Introduction to Russell. Technical report, Cornell University, 1989.
• Bet98: Gustavo Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computing Science, University of GSteborg, GSteborg, Sweden, February 1998.
• Car88: Luca Gardelli. Phase Distinction in Type Theory. Research report, DEC SRC, 1988.
• Car94: Luca Cardelli. The Quest Language and System. Research report, DEC SRC, 1994.
• CH86: Thierry Coquand and G~rard Huet. The Calculus of Constructions. Technical Report 530, INRIA, Centre de Rocquencourt, 1986.
• CH88: Thierry Coquand , Gerard Huet, The calculus of constructions, Information and Computation, v.76 n.2-3, p.95-120, February/March 1988 [doi>10.1016/0890-5401(88)90005-3]
• Con86: R. L. Constable , S. F. Allen , H. M. Bromley , W. R. Cleaveland , J. F. Cremer , R. W. Harper , D. J. Howe , T. B. Knoblock , N. P. Mendler , P. Panangaden , J. T. Sasaki , S. F. Smith, Implementing mathematics with the Nuprl proof development system, Prentice-Hall, Inc., Upper Saddle River, NJ, 1986
• Dan98: Olivier Danvy. Formatting Strings in ML. Technical Report RS-98-5, BRICS, Department of Computer SCience, University of Aarhus, Denmark, March 1998.
• Fra91: Frank Pfenning, Logic programming in the LF logical framework, Logical frameworks, Cambridge University Press, New York, NY, 1991
• HHP93: Robert Harper , Furio Honsell , Gordon Plotkin, A framework for defining logics, Journal of the ACM (JACM), v.40 n.1, p.143-184, Jan. 1993 [doi>10.1145/138027.138060]
• How80: W.A. Howard. Tile formulae-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors, To H.B. Curry: Essays on Uombinatory Logic, Lambda Calculus and Formalism, pages 479-490. Academic Press, London, 1980.
• Hud92: Paul Hudak , Simon Peyton Jones , Philip Wadler , Brian Boutel , Jon Fairbairn , Joseph Fasel , María M. Guzmán , Kevin Hammond , John Hughes , Thomas Johnsson , Dick Kieburtz , Rishiyur Nikhil , Will Partain , John Peterson, Report on the programming language Haskell: a non-strict, purely functional language version 1.2, ACM SIGPLAN Notices, v.27 n.5, p.1-164, May 1992 [doi>10.1145/130697.130699]
• Jon94: Mark P. Jones. The implementation of the Gofer filnctional programming system. Technical Report YALEU/DCS/RR-1030, Department of Computer Science, Yale University, New Haven, Connecticut, USA, May 1994, May 94.
• Lil97: Mark Lillibridge. Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1997. CM U-CS-97-122.
• LP92: Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. Technical report, LFCS Technical Report ECS-LFCS-92- 211, 1992.
• MN94: Lena Magnusson , Bengt Nordström, The ALF proof editor and its proof engine, Proceedings of the international workshop on Types for proofs and programs, p.213-237, January 1994, Nijmegen, The Netherlands
• Mor95: Greg Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, 1995.
• MTH90: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• Nor93: Bengt NordstrSm. The ALF proof editor. In Proceedings 1993 Informal Proceedings of the Nijmegen workhop on Types for Proofs and Programs, 1993.
• NPS90: Bengt Nordström , Kent Petersson , Jan M. Smith, Programming in Martin-Lo¨f's type theory: an introduction, Clarendon Press, New York, NY, 1990
• Pfe89: F. Pfening, Elf: a language for logic definition and verified metaprogramming, Proceedings of the Fourth Annual Symposium on Logic in computer science, p.313-322, June 1989, Pacific Grove, California, United States
• PJ93: John Peterson , Mark Jones, Implementing type classes, Proceedings of the ACM SIGPLAN 1993 conference on Programming language design and implementation, p.227-236, June 21-25, 1993, Albuquerque, New Mexico, United States
• Pol94: Robert Pollack. The Theory of Lego A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.
• TMC+96: David Tarditi, Greg Morrisett, Pery Cheng, Chris Stone, Robert Harper, and Peter Lee. TIL: A Type-directed Optimizing Compiler for ML. Technical Report CMU-CS-96-108, School of Computer Science, Carnegie Mellon University, February 1996.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Modules and interfaces
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Computability theory

General Terms:
Design, Languages, Performance, Theory

Keywords:
dependent types, language design, module systems, type systems