Advertisement

Cayenne — A Language with Dependent Types

  • Lennart Augustsson
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1608)

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.

Keywords

Type systems language design dependent types module systems 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. ACN90.
    Augustsson, L., Coquand, T., Nordström, B.: A short description of Another Logical Framework. In: Proceedings of the First Workshop on Logical Frameworks, Antibes, pp. 39–42 (1990)Google Scholar
  2. AJ89.
    Augustsson, L., Johnsson, T.: The Chalmers Lazy-ML Compiler. The Computer Journal 32(2), 127–141 (1989)CrossRefGoogle Scholar
  3. Aug93.
    Augustsson, L.: Implementing Haskell Overloading. In: Proc. 6th Int’l Conf. on Functional Programming Languages and Computer Architecture (FPCA 1993), pp. 65–73. ACM Press, New York (1993)CrossRefGoogle Scholar
  4. BDD89.
    Boehm, H., Demers, A., Donahue, J.: A Programmer’s Introduction to Russell. Technical report, Cornell University (1989)Google Scholar
  5. Bet98.
    Betarte, G.: Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computing Science, University of Göteborg, Göteborg, Sweden (February 1998)Google Scholar
  6. Car88.
    Cardelli, L.: Phase Distinction in Type Theory. Research report, DEC SRC (1988)Google Scholar
  7. Car94.
    Cardelli, L.: The Quest Language and System. Research report, DEC SRC (1994)Google Scholar
  8. CH86.
    Coquand, T., Huet, G.: The Calculus of Constructions. Technical Report 530, INRIA, Centre de Rocquencourt(1986)Google Scholar
  9. CH88.
    Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76(2/3), 95–120 (1988)zbMATHCrossRefMathSciNetGoogle Scholar
  10. Con86.
    Constable, R.L., et al.: Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs (1986)Google Scholar
  11. Dan98.
    Danvy, O.: Formatting Strings in ML. Technical Report RS-98-5, BRICS, Department of Computer SCience, University of Aarhus, Denmark (March 1998)Google Scholar
  12. Fra91.
    Logical Frameworks. Logic programming in the LF logical framework. In: Huet, G., Plotkin, G. (eds.) LICS 1989, pp. 149–181. Cambridge University Press, Cambridge (1991)Google Scholar
  13. HHP93.
    Harper, R., Honsell, F., Plotkin, G.: A Framework for Defining Logics. JACM 40(1), 143–184 (1993)zbMATHCrossRefMathSciNetGoogle Scholar
  14. How80.
    Howard, W.A.: The formulae-as-types notion of construction. In: Seldin, J.P., Hindley, J.R. (eds.) To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pp. 479–490. Academic Press, London (1980)Google Scholar
  15. Hud92.
    Hudak, P., et al.: Report on the Programming Language Haskell: A Non- Strict, Purely Functional Language (March 1992). Version 1.2. Also in Sigplan Notices (May 1992)Google Scholar
  16. Jon94.
    Jones, M.P.: The implementation of the Gofer functional programming system. Technical Report YALEU/DCS/RR-1030, Department of Computer Science, Yale University, New Haven, Connecticut, USA(May 1994)Google Scholar
  17. Lil97.
    Lillibridge, M.: Translucent Sums: A Foundation for Higher-Order Module Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, CMU-CS-97-122 (May 1997)Google Scholar
  18. LP92.
    Luo, Z., Pollack, R.: LEGO Proof Development System: User’s Manual. Technical report, LFCS Technical Report ECS-LFCS-92-211 (1992)Google Scholar
  19. MN94.
    Magnusson, L., Nordström, B.: The ALF proof editor and its proof engine. In: Types for Proofs and Programs, Nijmegen. LNCS, pp. 213–237. Springer, Heidelberg (1994)Google Scholar
  20. Mor95.
    Morrisett, G.: Compiling with Types. PhD thesis, Carnegie Mellon University (1995)Google Scholar
  21. MTH90.
    Milner, R., Tofte, M., Harper, R.: The Definition of Standard ML. MIT Press, Cambridge (1990)Google Scholar
  22. Nor93.
    Nordström, B.: The ALF proof editor. In: Proceedings 1993 Informal Proceedings of the Nijmegen workhop on Types for Proofs and Programs (1993)Google Scholar
  23. NPS90.
    Nordström, B., Petersson, K., Smith, J.M.: Programming in Martin-Löf ’s Type Theory. An Introduction. Oxford University Press, Oxford (1990)zbMATHGoogle Scholar
  24. Pfe89.
    Pfenning, F.: Elf: A language for logic definition and verified metaprogramming. In: LICS 1989, pp. 313–322. IEEE, Los Alamitos (1989)Google Scholar
  25. PJ93.
    Peterson, J., Jones, M.P.: Implementing Type Classes. In: Proceedings of ACM SIGPLAN Symposium on Programming Language Design and Implementation (1993)Google Scholar
  26. Pol94.
    Pollack, R.: The Theory of Lego A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh (1994)Google Scholar
  27. TMC+96.
    Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., Lee, P.: TIL: A Type-directed Optimizing Compiler for ML. Technical Report CMU-CS-96-108, School of Computer Science, Carnegie Mellon University (February 1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • Lennart Augustsson
    • 1
  1. 1.Department of Computing SciencesChalmers University of TechnologyGöteborgSweden

Personalised recommendations