Haskell Type System Analysis


  • Rafael Castro G. Silva Universidade do Estado de Santa Catarina
  • Karina Girardi Roggia Professora no curso de Bacharelado em Ciência da Computação da Universidade do Estado de Santa Catarina http://orcid.org/0000-0001-5194-5870
  • Cristiano Damiani Vasconcellos Professor no curso de Bacharelado em Ciência da Computação da Universidade do Estado de Santa Catarina




Haskell, Categorias, Lógica, Tipos


Types systems of programming languages are becoming more and more sophisticated and, in some cases, they are based on concepts from Logic, Type Theory and Category Theory. Haskell is a language with a modern type system and it is often singled out as an example using such theories. This work presents a small formalization of the Haskell type system and an analysis based on the mentioned theories, including its relation with the Intuitionist Propositional Second Order Logic and its logical characteristics, if there is a category in its type system and how monads are just monoids in the category of Haskell's endofunctors.


Download data is not yet available.

Author Biography

Rafael Castro G. Silva, Universidade do Estado de Santa Catarina

Estudante de mestrado em computação aplicada da Universidade do Estado de Santa Catarina


DAMAS, L.; MILNER, R. Principal type-schemes for functional programs. In: DEMILLO, R. (Ed.). Proceedings of the 9th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, USA: ACM, 1982. (POPL ’82).

WADLER, P. Propositions as types. Commun. ACM, v. 58, n. 12, p. 75–84, 2015.

HOWARD, W. A. The formulas-as-types notion of construction. In: SELDIN, J. P.; HINDLEY, J. R. (Ed.). To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism. 1. ed. New York, USA: Academic Press, 1980, (POPL, ’80). p. 479–490.

LAMBEK, J.; SCOTT, P. Introduction to Higher-Order Categorical Logic. 1. ed. Cambridge, UK: Cambridge University Press, 1988. v. 1. (Cambridge Studies in Advanced Mathematics, v. 1).

JONES, S. P. Haskell 98 language and libraries : the revised report. 1. ed. Cambridge, UK: Cambridge University Press, 2003.

WADLER, P.; BLOTT, S. How to make ad-hoc polymorphism less ad hoc. In: YORK, C. N. (Ed.). Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. New York, NY, USA: ACM, 1989. (POPL, ’89).

KFOURY, A. J.; TIURYN, J.; URZYCZYN, P. The undecidability of the semi-unification problem. In: ORTIZ, H. (Ed.). Proceedings of the Twenty-second Annual ACM Symposium on Theory of Computing. Baltimore, USA: ACM, 1990. (STOC, ’90).

FERNANDES, F. L. O Isomorfismo de Curry-Howard via Teoria de Categorias. 2011. Monography.

MOGGI, E. Computational lambda-calculus and monads. In: IEEE. Logic in Computer Science, 1989. Pacific Grove, USA: IEEE, 1989. (4).

WADLER, P. Comprehending monads. In: KAHN, G. (Ed.). Proceedings of the 1990 ACM conference on LISP and functional programming. New York, USA: ACM, 1990. v. 1.

WADLER, P. Monads for functional programming. In: JEURING, E. M. J. (Ed.). Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text. London, UK: Springer-Verlag, 1995. v. 1.

GENTZEN, G. Investigations into logical deduction. In: SZABO, M. E. (Ed.). The Collected Papers of Gerhard Gentzen. 1. ed. Amsterdam: North-Holland, 1969. v. 1, p. 68–213.

MENEZES, P.; HAEUSLER, E. H. Teoria das Categorias para Ciência da Computação. 1. ed. Porto Alegre, Brazil: Editora Sagra Luzzatto, 2001. v. 12. (Livros, v. 12).

SØRENSEN, M. H. B.; URZYCZYN, P. Lectures on the Curry-Howard Isomorphism. 1998.

GIRARD, J.-Y. Interpretation fonctionelle et elimination des coupures de l’arithmetique d’ordre superieur. Tese (Doutorado) — PhD thesis, Université Paris VII, Paris, France, 1972.

REYNOLDS, J. C. Towards a theory of type structure. In: Programming Symposium, Proceedings Colloque Sur La Programmation. Berlin, Heidelberg: Springer-Verlag, 1974. (LNCS, v. 29).

COSTA, N. C. d.; ABE, J. M. Paraconsistencia em informatica e inteligencia artificial. Estud. Av.

PIERCE, B. C. Types and Programming Languages. 1st. ed. Cambridge, USA: The MIT Press, 2002. v. 1.

REYNOLDS, J. C. Types, abstraction and parametric polymorphism. In: IFIP Congress. Berlin, Germany: Springer, 1983. (LNCS, v. 598).

HASKELLWIKI. HaskellWiki. 2017. Https://wiki.haskell.org/Hask.

BAUER, A. Mathematics and Computation - Hask is not a category. 2017. Http://math.andrej.com/2016/08/06/hask-is- not-a-category.

LANE, S. M.; LANE, S. M. Categories for the Working Mathematician. 2. ed. Berlin, Germany: Springer New York, 1998. v. 5. (Graduate Texts in Mathematics, v. 5).




How to Cite

Silva, R. C. G., Roggia, K. G., & Vasconcellos, C. D. (2018). Haskell Type System Analysis. Revista De Informática Teórica E Aplicada, 25(3), 75–88. https://doi.org/10.22456/2175-2745.82395



Selected Papers - WEIT 2017