Haskell Type System Analysis

Rafael Castro G. Silva, Karina Girardi Roggia, Cristiano Damiani Vasconcellos

Abstract


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.


Keywords


Haskell; Categorias; Lógica; Tipos

Full Text:

PDF

References


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).




DOI: https://doi.org/10.22456/2175-2745.82395

Copyright (c) 2018 Rafael Castro G. Silva, Karina Girardi Roggia, Cristiano Damiani Vasconcellos

Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.