Scrap Your Type Applications

  • Barry Jay
  • Simon Peyton Jones
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5133)


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.


Type Application Reduction Rule Functional Programming Critical Pair Type Inference 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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
  2. 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
  3. 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
  4. Girard, J.-Y., Lafont, Y., Taylor, P.: Proofs and Types. Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (1989)zbMATHGoogle Scholar
  5. 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
  6. 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-1Google Scholar
  7. 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), CrossRefGoogle Scholar
  8. Jay, C.B.: Typing first-class patterns. In: Higher-Order Rewriting, electronic proceedings (2006),
  9. 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-243zbMATHMathSciNetCrossRefGoogle Scholar
  10. 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)CrossRefGoogle Scholar
  11. Milner, R.: A theory of type polymorphism in programming. JCSS 13(3) (December 1978)Google Scholar
  12. 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)CrossRefGoogle Scholar
  13. Murphy, T.: The wizard of TILT: efficent, convenient, and abstract type representations. Technical Report CMU-CS-02-120, Carnegie Mellon University (2002),
  14. Necula, G.C., Lee, P.: Efficient representation and validation of proofs. In: Logic in Computer Science, pp. 93–104 (1998),
  15. 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),
  16. Petersen, L.: Certifying Compilation for Standard ML in a Type Analysis Framework. PhD thesis, Carnegie Mellon University (2005),
  17. Jones, S.P.: Haskell 98 language and libraries: the revised report. Cambridge University Press, Cambridge (2003)Google Scholar
  18. 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),
  19. Jones, S.P., Vytiniotis, D., Weirich, S., Shields, M.: Practical type inference for arbitrary-rank types. Journal of Functional Programming 17, 1–82 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  20. 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)CrossRefGoogle Scholar
  21. 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)CrossRefGoogle Scholar
  22. Reynolds, J.: Towards a theory of type structure. In: Robinet, B. (ed.) Programming Symposium 1974. LNCS, vol. 19. Springer, Heidelberg (1974)Google Scholar
  23. Saha, B., Shao, Z.: Optimal type lifting. In: Types in Compilation, pp. 156–177 (1998),
  24. 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
  25. 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
  26. 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)CrossRefGoogle Scholar
  27. Tolmach, A.: Tag-free garbage collection using explicit type parameters. In: ACM Symposium on Lisp and Functional Programming, pp. 1–11. ACM, Orlando (1994)CrossRefGoogle Scholar
  28. 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
  29. 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

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Barry Jay
    • 1
  • Simon Peyton Jones
    • 2
  1. 1.University of TechnologySydney 
  2. 2.Microsoft Research Cambridge 

Personalised recommendations