Functional un|unparsing

Kenichi Asai, Oleg Kiselyov, Chung Chieh Shan

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)


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 languageEnglish
Pages (from-to)311-340
Number of pages30
JournalHigher-Order and Symbolic Computation
Issue number4
Publication statusPublished - 2011 Nov


  • Continuations
  • Delimited control
  • Functional programming
  • Program derivation
  • Typed printf
  • Typed scanf


Dive into the research topics of 'Functional un|unparsing'. Together they form a unique fingerprint.

Cite this