Strongly typed memory areas programming systems-level data structures in a functional language

ABSTRACT

Modern functional languages offer several attractive features to support development of reliable and secure software. However, in our efforts to use Haskell for systems programming tasks-including device driver and operating system construction-we have also encountered some significant gaps in functionality. As a result, we have been forced, either to code some non-trivial components in more traditional but unsafe languages like C or assembler, or else to adopt aspects of the foreign function interface that compromise on strong typing and type safety.In this paper, we describe how we have filled one of these gaps by extending a Haskell-like language with facilities for working directly with low-level, memory-based data structures. Using this extension, we are able to program a wide range of examples, including hardware interfaces, kernel data structures, and operating system APIs. Our design allows us to address concerns about representation, alignment, and placement (in virtual or physical address spaces) that are critical in some systems applications, but clearly beyond the scope of most existing functional languages.Our approach leverages type system features that are wellknown and widely supported in existing Haskell implementations, including kinds, multiple parameter type classes, functional dependencies, and improvement. One interesting feature is the use of a syntactic abbreviation that makes it easy to define and work with functions at the type level.

REFERENCES

• 1: Godmar Back, DataScript - A Specification and Scripting Language for Binary Data, Proceedings of the 1st ACM SIGPLAN/SIGSOFT conference on Generative Programming and Component Engineering, p.66-77, October 06-08, 2002
• 2: Matthias Blume. No-Longer-Foreign: Teaching an ML compiler to speak C "natively". In BABEL 2001: 1st Workshop on Multi-Language Infrastructure and Interoperability, September 2001.
• 3: 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
• 4: Iavor S. Diatchki , Mark P. Jones , Rebekah Leslie, High-level views on low-level representations, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 5: Sigbjorn Finne , Daan Leijen , Erik Meijer , Simon Peyton Jones, H/Direct: a binary foreign language interface for Haskell, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.153-162, September 26-29, 1998, Baltimore, Maryland, United States
• 6: Kathleen Fisher , Robert Gruber, PADS: a domain-specific language for processing ad hoc data, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 7: Kathleen Fisher, Ricardo Pucella, and John Reppy. A framework for interoperability. In BABEL 2001: 1st Workshop on Multi-Language Infrastructure and Interoperability, September 2001.
• 8: Daniel Joeseph Grossman. Safe Programming at the C Level of Abstraction. PhD thesis, Cornell University, 2003.
• 9: Thomas Hallgren , Mark P. Jones , Rebekah Leslie , Andrew Tolmach, A principled approach to operating system construction in Haskell, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 10: Robert Harper, Peter Lee, and Frank Pfenning. The fox project: Advanced language technology for extensible systems. Technical Report CMU-CS-98-107, School of Computer Science, Carnegie Mellon University, January 1998.
• 11: Intel Corporation. IA-32 Intel Architecture Software Developer's Manual, Volumes 1-3. Available online from http://www.intel.com/design/Pentium4/documentation.htm.
• 12: Trevor Jim , J. Greg Morrisett , Dan Grossman , Michael W. Hicks , James Cheney , Yanling Wang, Cyclone: A Safe Dialect of C, Proceedings of the General Track: 2002 USENIX Annual Technical Conference, p.275-288, June 10-15, 2002
• 13: Mark P. Jones. Simplifying and improving qualified types. Technical Report YALEU/DCS/RR-1040, Yale University, New Haven, Connecticut, USA, June 1994.
• 14: 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
• 15: Mark P. Jones, Magnus Carlsson, and Johan Nordlander. Composed, and in Control: Programming the Timber Robot. Technical report, OGI School of Science & Engineering at OHSU, August 2002.
• 16: Simon Peyton Jones, editor. Haskell 98 Language and Libraries, The Revised Report. Cambridge University Press, 2003.
• 17: Brian W. Kernighan , Dennis M. Ritchie, The C programming language, Prentice Hall Press, Upper Saddle River, NJ, 1989
• 18: Xavier Leroy. CamlIDL User's Manual (Version 1.05). INRIA Rocquencourt.
• 19: Xiaoming Liu , Christoph Kreitz , Robbert van Renesse , Jason Hickey , Mark Hayden , Kenneth Birman , Robert Constable, Building reliable, high-performance communication systems from components, Proceedings of the seventeenth ACM symposium on Operating systems principles, p.80-92, December 12-15, 1999, Charleston, South Carolina, United States
• 20: Matthias Neubauer, Peter Thiemann, Martin Gasbichler, and Michael Sperber. A functional notation for functional dependencies. In Proceedings of The 2001 ACM SIGPLAN Haskell Workshop, Firenze, Italy, September 2001.
• 21: Norman Ramsey , Mary F. Fernández, Specifying representations of machine instructions, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.3, p.492-524, May 1997 [doi>10.1145/256167.256225]
• 22: Bjarne Stroustrup, The C++ Programming Language, Third Edition, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1997
• 23: Cyclone Team. Cyclone User's Manual (0.8.2), August 2004.
• 24: Haskell FFI Team. Haskell 98 Foreign Function Interface (1.0), 2003.
• 25: L4ka Team. L4 eXperimental Kernel Reference Manual, January 2005. Available online from http://l4ka.org/.
• 26: Andrew Tolmach , Dino P. Oliva, From ML to Ada: Strongly-typed language interoperability via source translation, Journal of Functional Programming, v.8 n.4, p.367-412, July 1998 [doi>10.1017/S0956796898003086]

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Data types and structures

General Terms:
Design, Languages

Keywords:
data representation, improvement, memory areas, memory manipulation, qualified types, systems programming