Isomorphisms, hylomorphisms and hereditarily finite data types in Haskell

ABSTRACT

This paper is an exploration in a functional programming framework of isomorphisms between elementary data types (natural numbers, sets, bitstrings, finite functions) and their extension to hereditarily finite universes through hylomorphisms derived from ranking and unranking operations. The paper is part of a larger effort to cover in a declarative programming paradigm some fundamental combinatorial generation algorithms along the lines of Knuth's recent work [10]. The self-contained source code of the paper, as generated from a literate Haskell program, is available at http://logic.csci.unt.edu/tarau/research/2008/sfISO.zip.

REFERENCES

• 1: Artem Alimarine , Sjaak Smetsers , Arjen van Weelden , Marko van Eekelen , Rinus Plasmeijer, There and back again: arrows for invertible programming, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.86-97, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088357]
• 2: Koen Claessen , John Hughes, Testing monadic code with QuickCheck, ACM SIGPLAN Notices, v.37 n.12, December 2002 [doi>10.1145/636517.636527]
• 3: Connan Eliot. Data. Bijections Haskell Module. http://haskell.org/haskellwiki/TypeCompose.
• 4: K. Gödel. Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik, 38:173--198, 1931.
• 5: Tim Harris , Simon Marlow , Simon Peyton Jones , Maurice Herlihy, Composable memory transactions, Communications of the ACM, v.51 n.8, August 2008 [doi>10.1145/1378704.1378725]
• 6: Juris Hartmanis , Theodore P. Baker, On Simple Goedel Numberings and Translations, Proceedings of the 2nd Colloquium on Automata, Languages and Programming, p.301-316, July 29-August 02, 1974
• 7: John Hughes, Generalising monads to arrows, Science of Computer Programming, v.37 n.1-3, p.67-111, May 2000 [doi>10.1016/S0167-6423(99)00023-4]
• 8: Graham Hutton, A tutorial on the universality and expressiveness of fold, Journal of Functional Programming, v.9 n.4, p.355-372, July 1999 [doi>10.1017/S0956796899003500]
• 9: R. Kaye and T. L. Wong. On Interpretations of Arithmetic and Set Theory. Notre Dame J. Formal Logic Volume, 48(4):497--510, 2007.
• 10: Donald E. Knuth, The Art of Computer Programming, Volume 4, Fascicle 4: Generating All Trees--History of Combinatorial Generation (Art of Computer Programming), Addison-Wesley Professional, 2006
• 11: John R. Koza, Genetic programming: on the programming of computers by means of natural selection, MIT Press, Cambridge, MA, 1992
• 12: C. Martinez and X. Molinero. Generic algorithms for the generation of combinatorial objects. In B. Rovan and P. Vojtas, editors, MFCS, volume 2747 of Lecture Notes in Computer Science, pages 572--581. Springer, 2003.
• 13: Erik Meijer , Graham Hutton, Bananas in space: extending fold and unfold to exponential types, Proceedings of the seventh international conference on Functional programming languages and computer architecture, p.324-333, June 26-28, 1995, La Jolla, California, United States [doi>10.1145/224164.224225]
• 14: Lawrence C. Paulson, A Concrete Final Coalgebra Theorem for ZF Set Theory, Selected papers from the International Workshop on Types for Proofs and Programs, p.120-139, June 06-10, 1994
• 15: Carla Piazza , Alberto Policriti, Ackermann encoding, bisimulations and OBDDs, Theory and Practice of Logic Programming, v.4 n.5-6, p.695-718, September 2004 [doi>10.1017/S1471068404002091]
• 16: M.-o. Takahashi. A Foundation of Finite Mathematics. Publ. Res. Inst. Math. Sci., 12(3):577--708, 1976.

INDEX TERMS

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

General Terms:
Algorithms, Languages

Keywords:
Ackermann encoding, Haskell data representations, computational mathematics, hereditarily finite functions, hereditarily finite sets, ranking/unranking