Abstract
Danvy's functional unparsing problem (Danvy in J. Funct. Program. 8(6), 621- 625, 1998) is to implement a type-safe 'printf' function, which converts a sequence of heterogeneous arguments to a string according to a given format. The dual problem is to implement a type-safe 'scanf' function, which extracts a sequence of heterogeneous arguments from a string by interpreting (Friedman and Wand in LFP, pp. 348-355, 1984 and in Essentials of Programming Languages, MIT Press, 2008) the same format as an equally heterogeneous sequence of patterns that binds zero or more variables. We derive multiple solutions to both problems (Wand in J. ACM 27(1), 164-180, 1980) from their formal specifications (Wand in Theor. Comput. Sci. 20(1), 3-32, 1982). On one hand, our solutions show how the Hindley-Milner type system, unextended, permits accessing heterogeneous sequences with the static assurance of type safety. On the other hand, our solutions demonstrate the use of control operators (Felleisen et al. in Proceedings of the 1988 ACMConference on Lisp and Functional Programming, pp. 52-62, ACMPress, New York, 1988; Wand in POPL 85: Conference Record of the Annual ACM Symposium on Principles of Programming Languages, vol. 16, ACMPress, New York, 1985; Meyer and Wand in Logics of Programs, Lecture Notes in Computer Science, vol. 193, pp. 219-224, Springer, Berlin, 1985) to communicate with formats as coroutines (Wand in Proceedings of the 1980 ACM Conference on Lisp and Functional Programming, vol. 12, pp. 285-299, ACM Press, New York, 1980 and Haynes et al. in LFP, pp. 293-298, 1984).
Original language | English |
---|---|
Pages (from-to) | 311-340 |
Number of pages | 30 |
Journal | Higher-Order and Symbolic Computation |
Volume | 24 |
Issue number | 4 |
DOIs | |
Publication status | Published - 2011 Nov |
Keywords
- Continuations
- Delimited control
- Functional programming
- Program derivation
- Typed printf
- Typed scanf
ASJC Scopus subject areas
- Software
- Computer Science Applications