Journal of Software, Vol 7, No 5 (2012), 1136-1148, May 2012
doi:10.4304/jsw.7.5.1136-1148

A New Paradigm for Component-based Development

Johan Georg Granström

Abstract


Hancock and Setzer describe how Haskell’s monolithic IO monad can be decomposed into worlds when working in a dependently typed language, like Martin-Löf’s type theory.

This paper introduces the notion of world map and shows that worlds and world maps form a category with arbitrary products. The construction of the category is carried out entirely in type theory and directly implementable in dependently typed programming languages.

If we let the notion of world replace the standard notion of interface, and the notion of world map replace the standard notion of component, we get a rigorous paradigm for component- based development. This new paradigm is investigated and several applications are given. For example, the problem of session state is given a very clean solution.



Keywords


functional constructs; components; functional programming; semantics of programming languages

References


 

[1] M. Abbott, T. Altenkirch, and N. Ghani. “Categories of Containers”. In: Foundations of Software Science and Computation Structures. Vol. 2620. Lect. Notes Comput. Sc. 2003, pp. 23–38.
http://dx.doi.org/10.1007/3-540-36576-1_2

[2] M. Abbott, T. Altenkirch, and N. Ghani. “Containers: Constructing strictly positive types”. In: Theor. Comput. Sci. 342 (2005), pp. 3–27.
http://dx.doi.org/10.1016/j.tcs.2005.06.002

[3] J. W. Backus. “Can programming be liberated from the von Neumann style? A functional style and its algebra of programs”. In: Communications of the ACM 21.8 (1978), pp. 613–641.
http://dx.doi.org/10.1145/359576.359579

[4] L. M. D. C. S. Barbosa. “Components as Coalgebras”. PhD thesis. Departamento de Informa ́tica, Escola de Engenharia, Universidade do Minho, 2001.

[5] A. Buisse and P. Dybjer. “The Interpretation of In- tuitionistic Type Theory in Locally Cartesian Closed Categories – an Intuitionistic Perspective”. In: Electron. Notes Theor. Comput. Sci. 218 (2008), pp. 21–32.
http://dx.doi.org/10.1016/j.entcs.2008.10.003

[6] P. Dybjer. “Inductive families”. In: Formal Aspects of Computing 6 (1994), pp. 440–465.
http://dx.doi.org/10.1007/BF01211308

[7] D. Garlan and M. Shaw. An Introduction to Software Architecture. Tech. rep. CMU-CS-94-166. School of Computer Science, Carnegie Mellon University, 1994.

[8] N. Ghani and T. Uustalu. “Coproducts of ideal monads”. In: Rairo Inf. Theor. Appl. 38.4 (2004), pp. 321–342.

[9] J. A. Goguen. “Categorical foundations for general sys- tems theory”. In: Proceedings of the European meeting, Vienna. Ed. by F. Pichler and R. Trappl. Advances in Cybernetics and Systems Research. Transcripta Books, 1972, pp. 121–130.

[10] P. Hancock and A. Setzer. “Interactive programs in dependent type theory”. In: Computer Science Logic. Vol. 1862. Lect. Notes Comput. Sc. 2000, pp. 317–331.
http://dx.doi.org/10.1007/3-540-44622-2_21

[11] P. Hoogendijk and O. de Moor. “Container types cat- egorically”. In: J. Funct. Programming 10.2 (2000), pp. 191–225.
http://dx.doi.org/10.1017/S0956796899003640

[12] P. Hudak et al. “A history of Haskell: being lazy with class”. In: Proceedings of the third ACM SIGPLAN con- ference on History of programming languages. HOPL III. New York, NY, USA: ACM, 2007, pp. 12-55.

[13] H. C. Lauer and R. M. Needham. “On the Duality of Operating System Structures”. In: Proc. Second Inter- national Symposium on Operating Systems. 1978.

[14] C. Lüth and N. Ghani. “Composing monads using coproducts”. In: ICFP. 2002, pp. 133–144.

[15] P. Martin-Löf. “Constructive mathematics and computer programming”. In: Logic, Methodology and Philosophy of Science VI. Ed. by L. J. Cohen et al. Amsterdam: North-Holland, 1982, pp. 153–175.

[16] P. Martin-Löf. Intuitionistic Type Theory. Studies in Proof Theory. Napoli: Bibliopolis, 1984.

[17] E. Moggi. “Computational lambda-calculus and mon- ads”. In: Proceedings of the Fourth Annual Symposium on Logic in computer science. Piscataway, NJ, USA: IEEE Press, 1989, pp. 14–23.

[18] B. Russell. “Mathematical Logic as Based on the Theory of Types”. In: Amer. J. Math. 30.3 (1908), pp. 222–262.
http://dx.doi.org/10.2307/2369948

[19] W. Swierstra. “Data types a` la carte”. In: J. Funct. Programming 18.4 (2008), pp. 423–436.
http://dx.doi.org/10.1017/S0956796808006758

[20] D. A. Turner. “Elementary strong functional program- ming”. In: First International Symposium on Functional Programming Languages in Education. Ed. by R. Plas- meijer and P. Hartel. Vol. 1022. 1995, pp. 1–13.


Full Text: PDF


Journal of Software (JSW, ISSN 1796-217X)

Copyright @ 2006-2014 by ACADEMY PUBLISHER – All rights reserved.