article

Free access

Cayenne—a language with dependent types

Author:

Lennart AugustssonAuthors Info & Claims

ACM SIGPLAN Notices, Volume 34, Issue 1

Pages 239 - 250

https://doi.org/10.1145/291251.289451

Published: 29 September 1998 Publication History

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

[1]

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.

[2]

L. Augustsson and T. Johnsson. The Chalmers Lazy-ML Compiler. The Computer Journal, 32(2):127-141, 1989.

Digital Library

[3]

Lenn~rt Augustsson. Implementing Haskell Overloading. ill Proc. 6th Int'l Conf. on Functional Programming Languages and Computer Architecture (FPCA'93), p~ges 65-73. ACM Press, June 1993.

Digital Library

[4]

H. Boehm, A. Demers, and J. Donahue. A Programmer's Introduction to Russell. Technical report, Cornell University, 1989.

[5]

Gustavo Betarte. Dependent Record Types and Algebraic Structures in Type Theory. PhD thesis, Department of Computing Science, University of GSteborg, GSteborg, Sweden, February 1998.

[6]

Luca Gardelli. Phase Distinction in Type Theory. Research report, DEC SRC, 1988.

[7]

Luca Cardelli. The Quest Language and System. Research report, DEC SRC, 1994.

[8]

Thierry Coquand and G~rard Huet. The Calculus of Constructions. Technical Report 530, INRIA, Centre de Rocquencourt, 1986.

[9]

Thierry Coquand and G~rard Huet. The Calculus of Constructions. Information and Computation, 76(2/3):9,5-120, 1988.

Digital Library

[10]

R.L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.

Digital Library

[11]

Olivier Danvy. Formatting Strings in ML. Technical Report RS-98-5, BRICS, Department of Computer SCience, University of Aarhus, Denmark, March 1998.

[12]

Logical Frameworks. Logic programming in the LF logical framework. In G~rard Huet and Gordon Plotkin, editors, L{CS'89, pages 149-181. Cambridge University Press, 1991.

Digital Library

[13]

Robert Harper, Furio Honsell, and Gordon Plotkin. A Framework for Defining Logics. JACM, 40(1):143-184, 1993.

Digital Library

[14]

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.

[15]

Paul Hudak 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.

Digital Library

[16]

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.

[17]

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.

[18]

Z. Luo and R. Pollack. LEGO Proof Development System: User's Manual. Technical report, LFCS Technical Report ECS-LFCS-92- 211, 1992.

[19]

Lena Magnusson and Bengt NordstrSm. The ALF proof editor and its proof engine. In Types for Proofs and Programs, LNCS, pages 213-237, Nijmegen, 1994. Springer-Verlag.

Digital Library

[20]

Greg Morrisett. Compiling with Types. PhD thesis, Carnegie Mellon University, 1995.

[21]

R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

Digital Library

[22]

Bengt NordstrSm. The ALF proof editor. In Proceedings 1993 Informal Proceedings of the Nijmegen workhop on Types for Proofs and Programs, 1993.

[23]

Bengt Nordstrsm, Kent Petersson, and Jan M. Smith. Programming in Martin-LSf 's Type Theory. An Introduction. Oxford University Press, 1990.

Digital Library

[24]

Frank Pfenning. Elf: A language for logic definition and verified meta-programming. In LICS'89, pages 313-322. IEEE, June 1989.

Digital Library

[25]

John Peterson and Mark P. Jones. Implementing Type Classes. In Proceedings of A CM SIGPLAN Symposium on Programming Language Design and Implementation, June 1993.

Digital Library

[26]

Robert Pollack. The Theory of Lego A Proof Checker for the Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1994.

[27]

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.

Cited By

Economou DKrishnaswami NDunfield J(2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/3610408Online publication date: 17-Oct-2023
https://doi.org/10.1145/3610408
Bird RGibbons JHinze RHöfner PJeuring JMeertens LMöller BMorgan CSchrijvers TSwierstra WWu N(2021)AlgorithmicsAdvancing Research in Information and Communication Technology10.1007/978-3-030-81701-5_3(59-98)Online publication date: 4-Aug-2021
https://doi.org/10.1007/978-3-030-81701-5_3
Li PZhang D(2018)A derivation framework for dependent security label inferenceProceedings of the ACM on Programming Languages10.1145/32764852:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276485
Show More Cited By

Index Terms

Cayenne—a language with dependent types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
        Modules / packages
      2. Language types
2. Theory of computation
  1. Models of computation
    1. Computability

Recommendations

Cayenne—a language with dependent types
ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

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) ...
Approximate normalization for gradual dependent types

Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it can be challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages. Gradual typing makes static type ...
Normalization by evaluation for sized dependent types

Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Copyright © 1998 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 September 1998

Published in SIGPLAN Volume 34, Issue 1

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

223
Total Citations
View Citations
1,544
Total Downloads

Downloads (Last 12 months)343
Downloads (Last 6 weeks)35

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Economou DKrishnaswami NDunfield J(2023)Focusing on Refinement TypingACM Transactions on Programming Languages and Systems10.1145/3610408Online publication date: 17-Oct-2023
https://doi.org/10.1145/3610408
Bird RGibbons JHinze RHöfner PJeuring JMeertens LMöller BMorgan CSchrijvers TSwierstra WWu N(2021)AlgorithmicsAdvancing Research in Information and Communication Technology10.1007/978-3-030-81701-5_3(59-98)Online publication date: 4-Aug-2021
https://doi.org/10.1007/978-3-030-81701-5_3
Li PZhang D(2018)A derivation framework for dependent security label inferenceProceedings of the ACM on Programming Languages10.1145/32764852:OOPSLA(1-26)Online publication date: 24-Oct-2018
https://dl.acm.org/doi/10.1145/3276485
Yang YPrestwood SBarnes C(2016)VizGenACM Transactions on Graphics10.1145/2980179.298240335:6(1-13)Online publication date: 5-Dec-2016
https://dl.acm.org/doi/10.1145/2980179.2982403
Yang YBi XOliveira B(2016)Unified Syntax with Iso-typesProgramming Languages and Systems10.1007/978-3-319-47958-3_14(251-270)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_14
Zhang DWang YSuh GMyers A(2015)A Hardware Design Language for Timing-Sensitive Information-Flow SecurityACM SIGARCH Computer Architecture News10.1145/2786763.269437243:1(503-516)Online publication date: 14-Mar-2015
https://dl.acm.org/doi/10.1145/2786763.2694372
Zhang DWang YSuh GMyers A(2015)A Hardware Design Language for Timing-Sensitive Information-Flow SecurityACM SIGPLAN Notices10.1145/2775054.269437250:4(503-516)Online publication date: 14-Mar-2015
https://dl.acm.org/doi/10.1145/2775054.2694372
Zhang DWang YSuh GMyers AOzturk OEbcioglu KDwarkadas S(2015)A Hardware Design Language for Timing-Sensitive Information-Flow SecurityProceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/2694344.2694372(503-516)Online publication date: 14-Mar-2015
https://dl.acm.org/doi/10.1145/2694344.2694372
Unno HTerauchi TKobayashi N(2013)Automating relatively complete verification of higher-order functional programsACM SIGPLAN Notices10.1145/2480359.242908148:1(75-86)Online publication date: 23-Jan-2013
https://dl.acm.org/doi/10.1145/2480359.2429081
Owens SSlind K(2008)Adapting functional programs to higher order logicHigher-Order and Symbolic Computation10.1007/s10990-008-9038-021:4(377-409)Online publication date: 1-Dec-2008
https://dl.acm.org/doi/10.1007/s10990-008-9038-0
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents