Many holes in hindley-milner

ABSTRACT

We implement statically-typed multi-holed contexts in OCaml using an underlying algebraic datatype augmented with phantom types. Existing approaches require dynamic checks or more complex type systems. In order to support concatenation we use two type parameters to represent the number of holes in a context as the difference between two Peano numbers. In order to support plugging a context with contexts of different arity we introduce a datatype of lists of contexts of length n with a total of m holes. Further, we extend our representation to allow holes to be marked with additional type information. As an example, we use these marks to implement statically-typed multi-holed XHTML contexts. We take advantage of Garrigue's relaxed value restriction.

REFERENCES

• 1: Thorsten Altenkirch, Conor McBride, and James McKinna. Why dependent types matter. Unpublished manuscript, April 2005. http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf.
• 2: Claus Braband , Anders Møller , Michael Schwartzbach, Static validation of dynamically generated HTML, Proceedings of the 2001 ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.38-45, June 2001, Snowbird, Utah, United States [doi>10.1145/379605.379657]
• 3: James Cheney and Ralf Hinze. First-class phantom types. Technical Report TR2003-1901, Cornell University, July 2003. http://ecommons.library.cornell.edu/handle/1813/5614.
• 4: Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. An idiom's guide to formlets. Technical Report EDI-INF-RR-1263, School of Informatics, University of Edinburgh, 2008a.
• 5: Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. The essence of form abstraction, 2008b. http://groups.inf.ed.ac.uk/links/formlets.
• 6: Olivier Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.242-257, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237784]
• 7: Olivier Danvy, Functional unparsing, Journal of Functional Programming, v.8 n.6, p.621-625, November 1998 [doi>10.1017/S0956796898003104]
• 8: Martin Elsman and Ken Friis Larsen. Typing XHTML web applications in ML. In PADL, pages 224--238, 2004.
• 9: Seth Fogarty , Emir Pasalic , Jeremy Siek , Walid Taha, Concoqtion: indexed types now!, Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 15-16, 2007, Nice, France [doi>10.1145/1244381.1244400]
• 10: Daniel Fridlender , Mia Indrika, Do we need dependent types?, Journal of Functional Programming, v.10 n.4, p.409-415, July 2000 [doi>10.1017/S0956796800003658]
• 11: Jacques Garrigue. Relaxing the value restriction. In FLOPS, pages 196--213, 2004.
• 12: Cordelia V. Hall , Kevin Hammond , Simon L. Peyton Jones , Philip Wadler, Type Classes in Haskell, Proceedings of the 5th European Symposium on Programming: Programming Languages and Systems, p.241-256, April 11-13, 1994
• 13: Haruo Hosoya , Benjamin C. Pierce, XDuce: A statically typed XML processing language, ACM Transactions on Internet Technology (TOIT), v.3 n.2, p.117-148, May 2003 [doi>10.1145/767193.767195]
• 14: Gérard Huet, The Zipper, Journal of Functional Programming, v.7 n.5, p.549-554, September 1997 [doi>10.1017/S0956796897002864]
• 15: R J M Hughes, A novel representation of lists and its application to the function "reverse", Information Processing Letters, v.22 n.3, p.141-144, March 1986 [doi>10.1016/0020-0190(86)90059-1]
• 16: 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
• 17: Conor McBride. The derivative of a regular type is its type of one--hole contexts. Unpublished manuscript, 2001. http://strictlypositive.org/diff.pdf.
• 18: Conor McBride, Faking it Simulating dependent types in Haskell, Journal of Functional Programming, v.12 n.5, p.375-392, July 2002 [doi>10.1017/S0956796802004355]
• 19: Anders Møller and Michael I. Schwartzbach. The design space of type checkers for XML transformation languages. In ICDT '05, January 2005.
• 20: D. Rémy, Type checking records and variants in a natural extension of ML, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.77-88, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75284]
• 21: Didier Rémy, Typing record concatenation for free, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.166-176, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143202]
• 22: Leon Sterling , Ehud Shapiro, The art of Prolog (2nd ed.): advanced programming techniques, MIT Press, Cambridge, MA, 1994
• 23: Peter Thiemann, A typed representation for HTML and XML documents in Haskell, Journal of Functional Programming, v.12 n.5, p.435-468, July 2002 [doi>10.1017/S0956796802004392]
• 24: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]
• 25: Hongwei Xi, Dependent ML An approach to practical programming with dependent types, Journal of Functional Programming, v.17 n.2, p.215-286, March 2007 [doi>10.1017/S0956796806006216]
• 26: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 27: 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
• 28: Zhe Yang, Encoding types in ML-like languages, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.289-300, September 26-29, 1998, Baltimore, Maryland, United States
• 29: Zhe Yang, Encoding types in ML-like languages, Theoretical Computer Science, v.315 n.1, p.151-190, 5 May 2004 [doi>10.1016/j.tcs.2003.11.017]
• 30: Christoph Zenger, Indexed types, Theoretical Computer Science, v.187 n.1-2, p.147-165, Nov. 15, 1997 [doi>10.1016/S0304-3975(97)00062-5]

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

General Terms:
Design, Languages

Keywords:
dependent type, indexed type, multi-holed context, phantom type, value restriction