Jana Dunfield
ABSTRACT
In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types. This system was shown sound with respect to a call-by-value operational semantics with effects, yet is inherently undecidable.In this paper we provide a decidable formulation for this system based on bidirectional checking, combining type synthesis and analysis following logical principles. The presence of unions and existential quantification requires the additional ability to visit subterms in evaluation position before the context in which they occur, leading to a tridirectional type system. While soundness with respect to the type assignment system is immediate, completeness requires the novel concept of contextual type annotations, introducing a notion from the study of principal typings into the source program.
- Alexander Aiken, Edward~L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In ACM Symp. Principles of Programming Languages, pages 163--173, 1994.]] Google Scholar
Digital Library
- Franco Barbanera, Mariangiola Dezani-Ciancaglini, and Ugo de'Liguoro. Intersection and union types: syntax and semantics. Inf. and Comp., 119:202--230, 1995.]] Google ScholarDigital Library
- R. Cartwright and M. Fagan. Soft typing. In SIGPLAN Conf. Programming Language Design and Impl. (PLDI), volume~26, pages 278--292, 1991.]] Google ScholarDigital Library
- M. Coppo, M. Dezani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeitschrift f. math. Logik und Grundlagen d. Math., 27:45--58, 1981.]]Google Scholar
- Rowan Davies. A practical refinement-type checker for Standard ML. In Algebraic Methodology and Software Tech. (AMAST'97), pages 565--566. Springer LNCS 1349, 1997.]] Google ScholarDigital Library
- Rowan Davies. Practical refinement-type checking. PhD thesis proposal, Carnegie Mellon University, 1997.]] Google ScholarDigital Library
- Rowan Davies and Frank Pfenning. Intersection types and computational effects. In Int'l Conf. Functional Programming (ICFP '00), pages 198--208, 2000.]] Google ScholarDigital Library
- Jana Dunfield. Combining two forms of type refinements. Technical Report CMU-CS-02-182, Carnegie Mellon University, September 2002.]]Google Scholar
- Jana Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In Found. Software Science and Computational Structures (FOSSACS '03), pages 250--266, Warsaw, Poland, April 2003. Springer LNCS 2620.]]Google ScholarCross Ref
- Tim Freeman. Refinement types for ML. PhD thesis, Carnegie Mellon University, 1994. CMU-CS-94-110.]] Google ScholarDigital Library
- Tim Freeman and Frank Pfenning. Refinement types for ML. In SIGPLAN Conf. Programming Language Design and Impl. (PLDI), volume 26, pages 268--277. ACM Press, 1991.]] Google ScholarDigital Library
- Haruo Hosoya and Benjamin~C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999.]]Google Scholar
- Trevor Jim. What are principal typings and what are they good for? Technical memorandum MIT/LCS/TM-532, MIT, November 1995.]] Google ScholarDigital Library
- Yitzhak Mandelbaum, David Walker, and Robert Harper. An effective theory of type refinements. Technical Report TR-656-02, Princeton, December 2002.]]Google Scholar
- Jens Palsberg and Christina Pavlopoulou. From polyvariant flow information to intersection and union types. J. Func. Prog., 11(3):263--317, 2001.]] Google ScholarDigital Library
- Benjamin C. Pierce. Programming with intersection types and bounded polymorphism. PhD thesis, Carnegie Mellon University, 1991. Technical Report CMU-CS-91-205.]] Google Scholar
- Benjamin C. Pierce. Programming with intersection types, union types, and polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.]]Google Scholar
- Benjamin C. Pierce and David N. Turner. Local type inference. In ACM Symp. Principles of Programming Languages, pages 252--265, 1998. Full version in ACM Trans. Prog. Lang. Sys., 22(1):1--44, 2000.]] Google ScholarDigital Library
- John C. Reynolds. Design of the programming language Forsythe. Technical Report CMU-CS-96-146, Carnegie Mellon University, 1996.]]Google Scholar
- Fred Smith, David Walker, and Greg Morrisett. Alias types. In European Symp. on Programming (ESOP'00), pages 366--381, Berlin, Germany, March 2000.]] Google ScholarDigital Library
- Jean-Pierre Talpin and Pierre Jouvelot. The type and effect discipline. Inf. and Comp., 111(2):245--296, 1994.]] Google ScholarDigital Library
- Mads Tofte and Jean-Pierre Talpin. Region-based memory management. Inf. and Comp., 132(2):109--176, 1997.]] Google ScholarDigital Library
- J. B. Wells and Christian Haack. Branching types. In European Symp. on Programming (ESOP'02), pages 115--132, 2002.]] Google ScholarDigital Library
- J.B. Wells, Allyn Dimock, Robert Muller, and Franklyn Turbak. A calculus with polymorphic and polyvariant flow types. J. Func. Prog., 12(3):183--317, May 2002.]] Google ScholarDigital Library
- Joe Wells. The essence of principal typings. In Int'l Coll. Automata, Languages, and Programming, volume 2380 of LNCS, pages 913--925. Springer, 2002.]] Google ScholarDigital Library
- Hongwei Xi. Dependent types in practical programming. PhD thesis, Carnegie Mellon University, 1998.]] Google ScholarDigital Library
- Hongwei Xi. Dependently typed data structures. Revision superseding WAAAPL '99, February 2000.]]Google Scholar
- Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In ACM Symp. Principles of Programming Languages, pages 214--227, 1999.]] Google ScholarDigital Library
Index Terms
- Tridirectional typechecking
Recommendations
Tridirectional typechecking
POPL '04In prior work we introduced a pure type assignment system that encompasses a rich set of property types, including intersections, unions, and universally and existentially quantified dependent types. This system was shown sound with respect to a call-by-...
Refined typechecking with Stardust
PLPV '07: Proceedings of the 2007 workshop on Programming languages meets program verificationWe present Stardust, an implementation of a type system for a subset of ML with type refinements, intersection types, and union types, enabling programmers to legibly specify certain classes of program invariants that are verified at compile time. This ...
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to ...
Comments