System F with type equality coercions

ABSTRACT

We introduce System FC, which extends System F with support for non-syntactic type equality. There are two main extensions: (i) explicit witnesses for type equalities, and (ii) open, non-parametric type functions, given meaning by top-level equality axioms. Unlike System F, FC is expressive enough to serve as a target for several different source-language features, including Haskell's newtype, generalised algebraic data types, associated types, functional dependencies, and perhaps more besides.

REFERENCES

• 1: Martín Abadi , Luca Cardelli , Pierre-Louis Curien, Formal parametric polymorphism, Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.157-170, March 1993, Charleston, South Carolina, United States [doi>10.1145/158511.158622]
• 2: Franz Baader , Tobias Nipkow, Term rewriting and all that, Cambridge University Press, New York, NY, 1999
• 3: Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.157-166, October 04-06, 2002, Pittsburgh, PA, USA
• 4: Val Breazu-Tannen , Thierry Coquand , Carl A. Gunter , Andre Scedrov, Inheritance as implicit coercion, Information and Computation, v.93 n.1, p.172-221, July 1991 [doi>10.1016/0890-5401(91)90055-7]
• 5: Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones, Associated type synonyms, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 6: Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones , Simon Marlow, Associated types with class, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 12-14, 2005, Long Beach, California, USA
• 7: C. Chen, D. Zhu, and H. Xi. Implementing cut elimination: A case study of simulating dependent types in Haskell. In Proc. of PADL'04, volume 3057 of LNCS, pages 239--254. Springer-Verlag, 2004.
• 8: Gang Chen, Coercive subtyping for the calculus of constructions, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.150-159, January 15-17, 2003, New Orleans, Louisiana, USA
• 9: James Cheney , Ralf Hinze, A lightweight implementation of generics and dynamics, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, p.90-104, October 03, 2002, Pittsburgh, Pennsylvania [doi>10.1145/581690.581698]
• 10: J. Cheney and R. Hinze. First-class phantom types. TR 1901, Cornell University, 2003.
• 11: Karl Crary, Typed compilation of inclusive subtyping, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.68-81, September 2000
• 12: Karl Crary , Stephanie Weirich, Flexible type analysis, Proceedings of the fourth ACM SIGPLAN international conference on Functional programming, p.233-248, September 27-29, 1999, Paris, France
• 13: Nachum Dershowitz , Jean-Pierre Jouannaud, Rewrite systems, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 14: Derek Dreyer , Karl Crary , Robert Harper, A type system for higher-order modules, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.236-249, January 15-17, 2003, New Orleans, Louisiana, USA
• 15: Derek Dreyer , Robert Harper , Manuel M. T. Chakravarty , Gabriele Keller, Modular type classes, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 16: G. J. Duck, S. Peyton Jones, P. J. Stuckey, and M. Sulzmann. Sound and decidable type inference for functional dependencies. In Proc. of (ESOP'04), number 2986 in LNCS, pages 49--63. Springer-Verlag, 2004.
• 17: Cordelia V. Hall , Kevin Hammond , Simon L. Peyton Jones , Philip L. Wadler, Type classes in Haskell, ACM Transactions on Programming Languages and Systems (TOPLAS), v.18 n.2, p.109-138, March 1996 [doi>10.1145/227699.227700]
• 18: R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. In Proc. of LICS'87, pages 194--204. IEEE Computer Society Press, 1987.
• 19: Robert Harper , John C. Mitchell, On the type structure of standard ML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.15 n.2, p.211-252, April 1993 [doi>10.1145/169701.169696]
• 20: Robert Harper , Greg Morrisett, Compiling polymorphism using intensional type analysis, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.130-141, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199475]
• 21: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 22: R. Kiessling and Z. Luo. Coercions in Hindley-Milner systems. In Types for Proofs and Programs: Third International Workshop, TYPES 2003, number 3085 in LNCS, pages 259--275, 2004.
• 23: J.-L. Lassez , M. J. Maher , K. Marriott, Unification revisited, Foundations of deductive databases and logic programming, Morgan Kaufmann Publishers Inc., San Francisco, CA, 1988
• 24: Konstantin Läfer , Martin Odersky, Polymorphic type inference and abstract data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1411-1430, Sept. 1994 [doi>10.1145/186025.186031]
• 25: D. R. Licata and R. Harper. A formulation of Dependent ML with explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie Mellon University, Dec. 2005.
• 26: P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis•Napoli, 1984.
• 27: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 28: John C. Mitchell, Polymorphic type inference and containment, Logical foundations of functional programming, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
• 29: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• 30: Emir Pasalic , Timothy E. Sheard, The role of type equality in meta-programming, OGI School of Science & Engineering, 2004
• 31: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 32: Benjamin C. Pierce, Types and programming languages, MIT Press, Cambridge, MA, 2002
• 33: B. Pierce, S. Dietzen, and S. Michaylov. Programming in higher-order typed lambda-calculi. Technical report, Carnegie Mellon University, 1989.
• 34: François Pottier , Yann Régis-Gianas, Stratified type inference for generalized algebraic data types, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 11-13, 2006, Charleston, South Carolina, USA
• 35: Zhong Shao , Valery Trifonov , Bratin Saha , Nikolaos Papaspyrou, A type system for certified binaries, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.1-45, January 2005 [doi>10.1145/1053468.1053469]
• 36: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 37: M. Sulzmann, M. M. T. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. Technical Report UNSW-CSE-TR-0624, The University of New South Wales, 2006. ftp://ftp.cse.unsw.edu.au/pub/doc/papers/UNSW/0624.pdf.
• 38: M. Sulzmann, T. Schrijvers, and P. J. Stuckey. Type inference for GADTs via Herbrand constraint abduction. http://www.comp.nus.edu.sg/~sulzmann, July 2006.
• 39: M. Sulzmann and M. Wang. A systematic translation of guarded recursive data types to existential types. Technical Report TR22/04, The National University of Singapore, 2004.
• 40: M. Sulzmann, J. Wazny, and P. J. Stuckey. A framework for extended algebraic data types. In Proc. of FLOPS'06, volume 3945 of LNCS, pages 47--64. Springer-Verlag, 2006.
• 41: Valery Trifonov , Bratin Saha , Zhong Shao, Fully reflexive intensional type analysis, Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.82-93, September 2000
• 42: Stephanie Weirich, Type-safe cast: (functional pearl), Proceedings of the fifth ACM SIGPLAN international conference on Functional programming, p.58-67, September 2000
• 43: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Languages, Theory

Keywords:
advanced type features, typed intermediate language