More Web Proxy on the site http://driver.im/

article

Dependent ML An approach to practical programming with dependent types

Author:

Hongwei XiAuthors Info & Claims

Journal of Functional Programming, Volume 17, Issue 2

Pages 215 - 286

https://doi.org/10.1017/S0956796806006216

Published: 01 March 2007 Publication History

Abstract

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML(${\cal L}$) language schema. This enrichment allows for specification and inference of significantly more precise type information, facilitating program error detection and compiler optimization. The primary contribution of the paper lies in our language design, which can effectively support the use of dependent types in practical programming. In particular, this design makes it both natural and straightforward to accommodate dependent types in the presence of effects such as references and exceptions.

References

[1]

Andrews, P. B. (1972) General Models, Descriptions and Choice in Type Theory. Journal of Symbolic Logic, 37, 385-394.

[2]

Andrews, P. B. (1986) An Introduction to Mathematical Logic: To Truth through Proof. Orlando, Florida: Academic Press.

[3]

Augustsson, L. (1998) Cayenne - a language with dependent types. Pages 239- 250 of: Proceedings of the 3rd ACM SIGPLAN International Conference on Functional Programming.

[4]

Barendregt, H. P. (1984) The lambda calculus, its syntax and semantics. Revised edition edn. Studies in Logic and the Foundations of Mathematics, vol. 103. Amsterdam: North-Holland.

[5]

Barendregt, H. P. (1992) Lambda Calculi with Types. Pages 117-441 of: Abramsky, S., Gabbay, Dov M., & Maibaum, T.S.E. (eds), Handbook of Logic in Computer Science, vol. II. Oxford: Clarendon Press.

[6]

Chen, C. & Xi, H. (2003) Implementing Typeful Program Transformations. Pages 20-28 of: Proceedings of ACM SIGPLAN Workshop on Partial Evaluation and Semantics based Program Manipulation.

[7]

Chen, C. & Xi, H. (2005a) Combining Programming with Theorem Proving. Pages 66- 77 of: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming.

[8]

Chen, C. & Xi, H. (2005b) Meta-Programming through Typeful Code Representation. Journal of Functional Programming, 15(6), 1-39.

[9]

Chen, C., Shi, R. & Xi, H. (2005) Implementing Typeful Program Transformations. Fundamenta informaticae, 69(1-2), 103-121.

[10]

Cheney, J. & Hinze, R. (2003) Phantom Types. Technical Report CUCIS-TR2003-1901. Cornell University. Available at http://techreports.library.cornell.edu:8081/ Dienst/UI/1.0/Display/cul.cis/TR2003-1901.

[11]

Church, A. (1940) A formulation of the simple type theory of types. Journal of Symbolic Logic, 5, 56-68.

[12]

Constable, R. L. et al.. (1986) Implementing Mathematics with the NuPrl Proof Development System. Englewood Cliffs, New Jersey: Prentice-Hall.

[13]

Dantzig, G. B. & Eaves, B. C. (1973) Fourier-Motzkin elimination and its dual. Journal of Combinatorial Theory (A), 14, 288-297.

[14]

Danvy, O. (1998) Functional unparsing. Journal of Functional Programming, 8(6), 621-625.

Digital Library

[15]

Dowek, G., Felty, A., Herbelin, H., Huet, G., Murthy, C., Parent, C., Paulin-Mohring, C. & Werner, B. (1993) The Coq proof assistant user's guide. Rapport Technique 154. INRIA, Rocquencourt, France. Version 5.8.

[16]

Dunfield, J. (2002) Combining two forms of type refinement. Tech. rept. CMU-CS-02-182. Carnegie Mellon University.

[17]

Dunfield, J. & Pfenning, F. (2003) Type assignment for intersections and unions in call-by-value languages. Pages 250-266 of: Gordon, A. D. (ed), Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'03). Warsaw, Poland: Springer-Verlag LNCS 2620.

[18]

Dunfield, J. & Pfenning, F. (2004) Tridirectional typechecking. Pages 281-292 of: Leroy, X. (ed), Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04). Venice, Italy: ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004.

[19]

Freeman, T. & Pfenning, F. (1991) Refinement types for ML. Pages 268-277 of: ACM SIGPLAN Conference on Programming Language Design and Implementation.

[20]

Girard, J.-Y. (1972) Interprétation fonctionnelle et Élimination des coupures dans l'arithmétique d'ordre supérieur. Thèse de doctorat d'état, Université de Paris VII, Paris, France.

[21]

Griffin, T. (1990) A Formulae-as-Types Notion of Control. Pages 47-58 of: Conference Record of POPL '90: 17th ACM SIGPLAN Symposium on Principles of Programming Languages.

[22]

Harper, R. (1994) A simplified account of polymorphic references. Information Processing Letters, 51, 201-206.

Digital Library

[23]

Hayashi, S. & Nakano, H. (1988) PX: A computational logic. The MIT Press.

[24]

Henkin, L. (1950) Completeness in the theory of types. Journal of Symbolic Logic, 15, 81-91.

[25]

Hinze, R. (2001) Manufacturing Datatypes. Journal of Functional Programming, 11(5), 493- 524.

Digital Library

[26]

Hughes, J., Pareto, L. & Sabry, A. (1996) Proving the Correctness of Reactive Systems Using Sized Types. Pages 410-423 of: Proceeding of 23rd Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '96).

[27]

INRIA. Objective Caml. http://caml.inria.fr.

[28]

Jay, C. B. & Sekanina, M. (1996) Shape checking of array programs. Tech. rept. 96.09. University of Technology, Sydney, Australia.

[29]

Jones, S. P., Vytiniotis, D., Weirich, S. & Washburn, G. (2005) Simple Unification-based Type Inference for GADTS.

[30]

Kahrs, S. (2001) Red-black trees with types. Journal of Functional Programming, 11(4), 425- 432.

Digital Library

[31]

Kreitz, C., Hayden, M. & Hickey, J. (1998) A proof environment for the development of group communication systems. Pages 317-332 of: Kirchner, H. & Kirchner, C. (eds), 15th International Conference on Automated Deduction. LNAI 1421. Lindau, Germany: Springer-Verlag.

[32]

Martin-Löf, P. (1984) Intuitionistic type theory. Naples, Italy: Bibliopolis.

[33]

Martin-Löf, P. (1985) Constructive mathematics and computer programming. Hoare, C. R. A. (ed), Mathematical logic and programming languages. Prentice-Hall.

[34]

McBride, C. Epigram. Available at: http://www.dur.ac.uk/CARG/epigram.

[35]

Meyer, A. & Wand, M. (1985) Continuation Semantics in Typed Lambda Calculi (summary). Pages 219-224 of: Parikh, R. (ed), Logics of Programs. Springer-Verlag LNCS 224.

[36]

Michaylov, S. (1992) Design and implementation of practical constraint logic programming systems. Ph.D. thesis, Carnegie Mellon University. Available as Technical Report CMU-CS-92-168.

[37]

Milner, R., Tofte, M., Harper, R. W. & MacQueen, D. (1997) The Definition of Standard ML (revised). Cambridge, Massachusetts: MIT Press.

[38]

Mitchell, J. C. & Plotkin, G. D. (1988) Abstract types have existential type. ACM Transactions on Programming Languages and Systems, 10(3), 470-502.

Digital Library

[39]

Mitchell, J. C. & Scott, P. J. (1989) Typed lambda models and cartesian closed categories (preliminary version). Pages 301-316 of: Gray, J. W. & Scedrov, A. (eds), Categories in Computer Science and Logic. Contemporary Mathematics, vol. 92. Boulder, Colorado: American Mathematical Society.

[40]

Odersky, M., Zenger, C. & Zenger, M. (2001) Colored Local Type Inference. Pages 41-53 of: Proceedings of the 28th Annual ACM SIGPPLAN-SIGACT Symposium on Principles of Programming Languages.

[41]

Okasaki, C. (1998) Purely Functional Data Structures. Cambridge University Press.

[42]

Owre, S., Rajan, S., Rushby, J. M., Shankar, N. & Srivas, M. K. (1996) PVS: Combining specification, proof checking, and model checking. Pages 411-414 of: Alur, R. & Henzinger, T. A. (eds), Proceedings of the 8th International Conference on Computer-Aided Verification (CAV'96). New Brunswick, NJ: Springer-Verlag LNCS 1102.

[43]

Parent, C. (1995) Synthesizing proofs from programs in the calculus of inductive constructions. Pages 351-379 of: Proceedings of the International Conference on Mathematics for Programs Constructions. Springer-Verlag LNCS 947.

[44]

Peyton Jones, S. et al.. (1999) Haskell 98 - A non-strict, purely functional language. Available at http://www.haskell.org/onlinereport/.

[45]

Pfenning, F. Computation and Deduction. Cambridge University Press. (To appear).

[46]

Pfenning, F. & Elliott, C. (1988) Higher-order abstract syntax. >Pages 199-208 of: Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation.

[47]

Pierce, B. & Turner, D. (1998) Local type inference. Pages 252-265 of: Proceedings of 25th Annual ACM SIGPLAN Symposium on Principles of Programming Languages (POPL '98).

[48]

Pottier, F. & Régis-Gianas, Y. (2006) Stratified type inference for generalized algebraic data types. Pages 232-244 of: Proceedings of the 33rd ACM Symposium on Principles of Programming Languages (POPL'06).

[49]

Pugh, W. & Wonnacott, D. (1992) Eliminating false data dependences using the Omega test. Pages 140-151 of: ACM SIGPLAN '92 Conference on Programming Language Design and Implementation. ACM Press.

[50]

Pugh, W. & Wonnacott, D. (1994) Experience with constraint-based array dependence analysis. Tech. rept. CS-TR-3371. University of Maryland.

[51]

Sannella, D. & Tarlecki, A. (1989) Toward formal development of ML programs: Foundations and methodology. Tech. rept. ECS-LFCS-89-71. Laboratory for Foundations of Computer Science, Department of Computer Science, University of Edinburgh.

[52]

Sheard, T. (2004) Languages of the future. Proceedings of the Onward! Track of Objected-oriented Programming Systems, Languages, Applications (OOPSLA). Vancouver, BC: ACM Press.

[53]

Shostak, R. E. (1977) On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4), 529-543.

Digital Library

[54]

Sulzmann, M., Odersky, M. & Wehr, M. (1997) Type inference with constrained types. Proceedings of 4th International Workshop on Foundations of Object-oriented Languages.

[55]

Takahashi, M. (1995) Parallel Reduction. Information & Computation, 118, 120-127.

Digital Library

[56]

Westbrook, E., Stump, A. & Wehrman, I. (2005) A Language-Based Approach to Functionally Correct Imperative Programming. Pages 268-279 of: Proceedings of the 10th ACM SIGPLAN International Conference on Functional Programming.

[57]

Wright, A. (1995) Simple imperative polymorphism. Journal of Lisp and Symbolic Computation, 8(4), 343-355.

Digital Library

[58]

Xi, H. (1998) Dependent types in practical programming. Ph.D. thesis, Carnegie Mellon University. pp. viii+189. Available at http://www.cs.cmu.edu/~hwxi/DML/thesis.ps.

[59]

Xi, H. (1999) Dependently Typed Data Structures. Pages 17-33 of: Proceedings of Workshop on Algorithmic Aspects of Advanced Programming Languages.

[60]

Xi, Hongwei. (2003). Dependently Typed Pattern Matching. Journal of Universal Computer Science, 9(8), 851-872.

[61]

Xi, H. (2004) Applied Type System (extended abstract). Pages 394-408 of: Post-Workshop Proceedings of Types 2003. Springer-Verlag LNCS 3085.

[62]

Xi, H. (2005) Applied Type System. Available at: http://www.cs.bu.edu/~hwxi/ATS.

[63]

Xi, H. & Pfenning, F. (1998) Eliminating array bound checking through dependent types. Pages 249-257 of: Proceedings of ACM SIGPLAN Conference on Programming Language Design and Implementation.

[64]

Xi, H. & Pfenning, F. (1999) Dependent Types in Practical Programming. Pages 214-227 of: Proceedings of 26th ACM SIGPLAN Symposium on Principles of Programming Languages. San Antonio, Texas: ACM press.

[65]

Xi, H., Chen, C. & Chen, G. (2003) Guarded Recursive Datatype Constructors. Pages 224- 235 of: Proceedings of the 30th ACM SIGPLAN Symposium on Principles of Programming Languages. New Orleans, LA: ACM press.

[66]

Zenger, C. (1997) Indexed types. Theoretical Computer Science, 187, 147-165.

Digital Library

[67]

Zenger, C. (1998) Indizierte typen. Ph.D. thesis, Fakultät für Informatik, Universität Karlsruhe.

Cited By

Lemay MFu QBlair WZhang CXi HCong YDagand P(2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609407
Fu QXi HCong YDagand P(2023)A Calculus of Inductive Linear ConstructionsProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609404(1-13)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609404
Cong YMilano MLeo J(2023)Weighted Refinement Types for Counterpoint CompositionProceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3609023.3609804(2-7)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609023.3609804
Show More Cited By

Index Terms

Dependent ML An approach to practical programming with dependent types
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program constructs
      1. Type structures

Recommendations

Dependent types in practical programming
Dependent types in practical programming
POPL '99: Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages

We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index objects are drawn from a constraint domain C, leading to the DML(C) language schema. This allows specification and inference of ...
Dependent Types at Work
Language Engineering and Rigorous Software Development

In these lecture notes we give an introduction to functional programming with dependent types. We use the dependently typed programming language Agda which is an extension of Martin-Löf type theory. First we show how to do simply typed functional ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of Functional Programming

Journal of Functional Programming Volume 17, Issue 2

March 2007

141 pages

ISSN:0956-7968

Issue’s Table of Contents

Publisher

Cambridge University Press

United States

Publication History

Published: 01 March 2007

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

41
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 23 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lemay MFu QBlair WZhang CXi HCong YDagand P(2023)A Dependently Typed Language with Dynamic EqualityProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609407(44-57)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609407
Fu QXi HCong YDagand P(2023)A Calculus of Inductive Linear ConstructionsProceedings of the 8th ACM SIGPLAN International Workshop on Type-Driven Development10.1145/3609027.3609404(1-13)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609027.3609404
Cong YMilano MLeo J(2023)Weighted Refinement Types for Counterpoint CompositionProceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3609023.3609804(2-7)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3609023.3609804
Pulte CMakwana DSewell TMemarian KSewell PKrishnaswami N(2023)CN: Verifying Systems C Code with Separation-Logic Refinement TypesProceedings of the ACM on Programming Languages10.1145/35711947:POPL(1-32)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571194
Nishida YSaito HChen RKawata AFuruse JSuenaga KIgarashi A(2022)Helmholtz: A Verifier for Tezos Smart Contracts Based on Refinement TypesNew Generation Computing10.1007/s00354-022-00167-140:2(507-540)Online publication date: 27-May-2022
https://dl.acm.org/doi/10.1007/s00354-022-00167-1
Sammler MLepigre RKrebbers RMemarian KDreyer DGarg DFreund SYahav E(2021)RefinedC: automating the foundational verification of C code with refined ownership typesProceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3453483.3454036(158-174)Online publication date: 19-Jun-2021
https://dl.acm.org/doi/10.1145/3453483.3454036
Rajani VGaboardi MGarg DHoffmann J(2021)A unifying type-theory for higher-order (amortized) cost analysisProceedings of the ACM on Programming Languages10.1145/34343085:POPL(1-28)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434308
Henriksen T(2021)Bounds Checking on GPUInternational Journal of Parallel Programming10.1007/s10766-021-00703-449:6(761-775)Online publication date: 1-Dec-2021
https://dl.acm.org/doi/10.1007/s10766-021-00703-4
Sekiyama TTsukada TIgarashi A(2020)Signature restriction for polymorphic algebraic effectsProceedings of the ACM on Programming Languages10.1145/34089994:ICFP(1-30)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408999
Chang SBallantyne MTurner MBowman W(2019)Dependent type systems as macrosProceedings of the ACM on Programming Languages10.1145/33710714:POPL(1-29)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371071
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents