Implicit parameters: dynamic scoping with static types

ABSTRACT

This paper introduces a language feature, called implicit parameters, that provides dynamically scoped variables within a statically-typed Hindley-Milner framework. Implicit parameters are lexically distinct from regular identifiers, and are bound by a special with construct whose scope is dynamic, rather than static as with let. Implicit parameters are treated by the type system as parameters that are not explicitly declared, but are inferred from their use. We present implicit parameters within a small call-by-name &lgr;-calculus. We give a type system, a type inference algorithm, and several semantics. We also explore implicit parameters in the wider settings of call-by-need languages with overloading, and call-by-value languages with effects. As a witness to the former, we have implemented implicit parameters as an extension of Haskell within the Hugs interpreter, which we use to present several motivating examples.

REFERENCES

• 1: BENTON, N. A mixed linear and non-linear logic: Proofs, terms and models. Tech. Rep. 352, University of Cambridge Computer Laboratory, Oct. 1994.
• 2: GARRIGUE, J. Dynamic binding and lexical binding in a transformation calculus. In Proc. of the Fuji International Workshop on Functional and Logic Programming. (1995).
• 3: Jacques Garrigue , Hassan Aït-Kaci, The typed polymorphic label-selective λ-calculus, Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.35-47, January 16-19, 1994, Portland, Oregon, United States [doi>10.1145/174675.174434]
• 4: HANSON, C. MIT Scheme Reference. Cambridge, MA: MIT Press, Apr. 96.
• 5: Mark P. Jones, Qualified types: theory and practice, Cambridge University Press, New York, NY, 1995
• 6: JONES, M. P. Exploring the design space for typebased implicit parameterization. Tech. rep., Oregon Graduate Institute, July 1999.
• 7: JONES, M. P. Type classes with functional dependencies, Oct. 1999. (Submitted for publication).
• 8: JONES, M. P., AND PETERSON, J. C. Hugs 98 user manual, http://~--~.haskell, org/hugs/, May 1999.
• 9: David J. King , John Launchbury, Structuring depth-first search algorithms in Haskell, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.344-354, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199530]
• 10: Sheng Liang, Java Native Interface: Programmer's Guide and Reference, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 11: MEIJER, E., AND CLAESSEN, K. The design and implementation of Mondrian. In Proceedings o/the HaskeU Workshop (1997).
• 12: Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
• 13: Martin Odersky , Philip Wadler , Martin Wehr, A second look at overloading, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.135-146, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224195]
• 14: PEYTON JONES, S., AND HUGHES, J. Haskell 98: A non-strict, purely functional language. http ://haskell. cs. yale. edu/onlinereport/, Jan. 1999.
• 15: 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]
• 16: P. Wadler , S. Blott, How to make ad-hoc polymorphism less ad hoc, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.60-76, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75283]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Algorithms, Design, Theory