Skip to main content
SpringerLink
Log in

Scrap Your Type Applications

  • Conference paper
Mathematics of Program Construction (MPC 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5133))

Included in the following conference series:

Abstract

System F is ubiquitous in logic, theorem proving, language meta-theory, compiler intermediate languages, and elsewhere. Along with its type abstractions come type applications, but these often appear redundant. This redundancy is both distracting and costly for type-directed compilers.

We introduce System IF, for implicit System F, in which many type applications can be made implicit. It supports decidable type checking and strong normalisation. Experiments with Haskell suggest that it could be used to reduce the amount of intermediate code in compilers that employ System F.

System IF constitutes a first foray into a new area in the design space of typed lambda calculi, that is interesting in its own right and may prove useful in practice.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  • Chilpala, A., Petersen, L., Harper, R.: Strict bidirectional type checking. In: ACM SIGPLAN International Workshop on Types in Language Design and Implementation (TLDI 2005), Long Beach. ACM Press, New York (2005)

    Google Scholar 

  • Coq. COQ (2007), http://pauillac.inria.fr/coq/

  • Ghani, N.: Eta-expansions in dependent type theory – the calculus of constructions. In: de Groote, P., Hindley, J.R. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 164–180. Springer, Heidelberg (1997)

    Google Scholar 

  • Girard, J.-Y.: The System F of variable types: fifteen years later. In: Huet, G. (ed.) Logical Foundations of Functional Programming. Addison-Wesley, Reading (1990)

    Google Scholar 

  • Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)

    MATH  Google Scholar 

  • Harper, R., Morrisett, G.: Compiling polymorphism using intensional type analysis. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, pp. 130–141 (January 1995)

    Google Scholar 

  • Hinze, R., Jones, S.P.: Derivable type classes. In: Hutton, G. (ed.) Proceedings of the 2000 Haskell Workshop, Montreal (September 2000); Nottingham University Department of Computer Science Technical Report NOTTCS-TR-00-1

    Google Scholar 

  • Jay, B., Kesner, D.: Pure Pattern Calculus. In: Sestoft, P. (ed.) ESOP 2006 and ETAPS 2006. LNCS, vol. 3924, pp. 100–114. Springer, Heidelberg (2006), www-staff.it.uts.edu.au/~cbj/Publications/purepatterns.pdf

    Chapter  Google Scholar 

  • Jay, C.B.: Typing first-class patterns. In: Higher-Order Rewriting, electronic proceedings (2006), http://hor.pps.jussieu.fr/06/proc/jay1.pdf

  • Jay, C.B., Ghani, N.: The virtues of eta-expansion. J. of Functional Programming 5(2), 135–154 (1995); Also appeared as tech. report ECS-LFCS-92-243

    Article  MATH  MathSciNet  Google Scholar 

  • Le Botlan, D., Rémy, D.: MLF: raising ML to the power of System F. In: ACM SIGPLAN International Conference on Functional Programming (ICFP 2003), Uppsala, Sweden, pp. 27–38. ACM Press, New York (2003)

    Chapter  Google Scholar 

  • Milner, R.: A theory of type polymorphism in programming. JCSS 13(3) (December 1978)

    Google Scholar 

  • Minamide, Y., Morrisett, G., Harper, R.: Typed closure conversion. In: 23rd ACM Symposium on Principles of Programming Languages (POPL 1996), St Petersburg Beach, Florida, pp. 271–283. ACM Press, New York (1996)

    Chapter  Google Scholar 

  • Murphy, T.: The wizard of TILT: efficent, convenient, and abstract type representations. Technical Report CMU-CS-02-120, Carnegie Mellon University (2002), http://reports-archive.adm.cs.cmu.edu/anon/2002/CMU-CS-02-120.pdf

  • Necula, G.C., Lee, P.: Efficient representation and validation of proofs. In: Logic in Computer Science, pp. 93–104 (1998), citeseer.ist.psu.edu/article/necula98efficient.html

  • Norell, U.: Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, Göteborg, Sweden (2007), http://www.cs.chalmers.se/~ulfn/papers/thesis.pdf

  • Petersen, L.: Certifying Compilation for Standard ML in a Type Analysis Framework. PhD thesis, Carnegie Mellon University (2005), http://reports-archive.adm.cs.cmu.edu/anon/2005/CMU-CS-05-135.pdf

  • Jones, S.P.: Haskell 98 language and libraries: the revised report. Cambridge University Press, Cambridge (2003)

    Google Scholar 

  • Jones, S.P., Hall, C., Hammond, K., Partain, W., Wadler, P.: The Glasgow Haskell Compiler: a technical overview. In: Proceedings of Joint Framework for Information Technology Technical Conference, Keele, DTI/SERC, pp. 249–257 (March 1993), http://research.microsoft.com/~simonpj/Papers/grasp-jfit.ps.Z

  • Jones, S.P., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. Journal of Functional Programming 17, 1–82 (2007)

    Article  MATH  MathSciNet  Google Scholar 

  • Pfenning, F.: Partial polymorphic type inference and higher-order unification. In: LFP 1988: Proceedings of the 1988 ACM conference on LISP and functional programming, pp. 153–163. ACM, New York (1988)

    Chapter  Google Scholar 

  • Pierce, B.C., Turner, D.N.: Local type inference. In: 25th ACM Symposium on Principles of Programming Languages (POPL 1998), San Diego, pp. 252–265. ACM, New York (1998)

    Chapter  Google Scholar 

  • Reynolds, J.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium 1974. LNCS, vol. 19. Springer, Heidelberg (1974)

    Google Scholar 

  • Saha, B., Shao, Z.: Optimal type lifting. In: Types in Compilation, pp. 156–177 (1998), http://citeseer.ist.psu.edu/article/saha98optimal.html

  • Shao, Z.: An overview of the FLINT/ML compiler. In: Proc. 1997 ACM SIGPLAN Workshop on Types in Compilation (TIC 1997), Amsterdam, The Netherlands (June 1997)

    Google Scholar 

  • Shao, Z., League, C., Monnier, S.: Implementing typed intermediate languages. In: ACM SIGPLAN International Conference on Functional Programming (ICFP 1998), ACM SIGPLAN Notices, Baltimore, vol. 34(1), pp. 106–119. ACM Press, New York (1998)

    Google Scholar 

  • Tarditi, D., Morrisett, G., Cheng, P., Stone, C., Harper, R., Lee, P.: TIL: A type-directed optimizing compiler for ML. In: ACM Conference on Programming Languages Design and Implementation (PLDI 1996), pp. 181–192. ACM, Philadelphia (1996)

    Chapter  Google Scholar 

  • Tolmach, A.: Tag-free garbage collection using explicit type parameters. In: ACM Symposium on Lisp and Functional Programming, pp. 1–11. ACM, Orlando (1994)

    Chapter  Google Scholar 

  • Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proc 16th ACM Symposium on Principles of Programming Languages, Austin, Texas. ACM Press, New York (1989)

    Google Scholar 

  • Wells, J.B.: Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In: Proceedings, Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Technology, Sydney,  

    Barry Jay

  2. Microsoft Research Cambridge,  

    Simon Peyton Jones

Authors
  1. Barry Jay
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Simon Peyton Jones
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Philippe Audebaud Christine Paulin-Mohring

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jay, B., Peyton Jones, S. (2008). Scrap Your Type Applications. In: Audebaud, P., Paulin-Mohring, C. (eds) Mathematics of Program Construction. MPC 2008. Lecture Notes in Computer Science, vol 5133. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70594-9_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-70594-9_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-70593-2

  • Online ISBN: 978-3-540-70594-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation