Abstract
Nowadays the support of generalized algebraic data types (GADTs) in extensions of Haskell allows functions defined over GADTs to be written without the need for type annotations in some cases and requires type annotations in other cases. In this paper we present a type inference algorithm for GADTs that is based on a closed-world approach to overloading and uses anti-unification and constraint-set satisfiability to infer the relationship between the types of function arguments and result. Through some examples, we show how the proposed algorithm allows more functions defined over GADTs to be written without the need for type annotations.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Camarão, C., Figueiredo, L.: Type inference for overloading without restrictions, declarations or annotations. In: Middeldorp, A., Sato, T. (eds.) FLOPS 1999. LNCS, vol. 1722, pp. 37–52. Springer, Heidelberg (1999)
Camarão, C., Figueiredo, L., Vasconcellos, C.: Constraint-set Satisfiability for Overloading. In: Proceedings of the 6th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pp. 67–77. ACM (2004)
Chang, C.C., Keisler, H.J.: Model Theory: Dover Books on Mathematics, 3rd edn. North-Holland Press, New York (2012)
Demoen, B., de la Banda, M.G., Stuckey, P.J.: Type Constraint Solving for Parametric and Ad-hoc Polymorphism. In: Proceedings of the 22nd Australasian Computer Science Conference (1999)
Jones, M.: Simplifying and Improving Qualified Types. In: Proceedings of ACM Conference on Functional Programming and Computer Architecture, FPCA 1995, pp. 160–169 (1995)
Jones, S.P., Vytiniotis, D., Weirich, S., Washburn, G.: Simple unification-based type inference for GADTs. SIGPLAN Not. 41(9), 50–61 (2006)
Jones, S.P., Washburn, G., Weirich, S.: Wobbly types: type inference for generalised algebraic data types. Technical report MS-CIS-05-26, University of Pennsylvania, Microsoft Research (2004). http://research.microsoft.com/apps/pubs/default.aspx?id=65143
Lin, C.K.: Practical type inference for the GADT type system. Ph.D. thesis, Portland State University, Portland, OR, USA (2010)
Lin, C.K., Sheard, T.: Pointwise generalized algebraic data types. In: Proceedings of the 5th ACM SIGPLAN Workshop on Types in Language Design and Implementation, TLDI 2010, pp. 51–62. ACM, New York (2010)
Plotkin, G.D.: A note on inductive generalisation. Mach. intell. 5(1), 153–163 (1970)
Plotkin, G.D.: A further note on inductive generalisation. Mach. Intell. 6, 101–124 (1971)
Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. SIGPLAN Not. 41(1), 232–244 (2006)
Ribeiro, R., Camarão, C.: Ambiguity and context-dependent overloading. J. Braz. Comput. Soc. 19(3), 313–324 (2013)
Ribeiro, R., Camarão, C., Figueiredo, L.: Terminating constraint set satisfiability and simplification algorithms for context-dependent overloading. J. Braz. Comput. Soc. 19(4), 423–432 (2013)
Schrijvers, T., Jones, S.P., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. SIGPLAN Not. 44(9), 341–352 (2009)
Smith, G.: Polymorphic type inference for languages with overloading and subtyping. Ph.D. thesis, Cornell University (1991)
Smith, G.: Principal type schemes for functional programs with overloading and subtyping. Sci. Comput. Program. 23(2–3), 197–226 (1994)
Stuckey, P., Sulzmann, M.: A Theory of overloading. In: Proceedings of the 7th ACM International Conference on Functional Programming, pp. 167–178 (2002)
Sulzmann, M., Schrijvers, T., Stuckey, P.J.: Type Inference for GADTs via Herbrand Constraint Abduction (2008)
Team, G., et al.: The Glorious Glasgow Haskell Compilation System User’s Guide, Version 7.10.1 (2015)
Vasconcellos, C.: Inferência de tipos com suporte para sobrecarga baseada no sistema CT. Ph.D. thesis, Universidade Federal de Minas Gerais, Minas Gerais, Brasil (2004)
Vytiniotis, D., Jones, S.P., Schrijvers, T., Sulzmann, M.: OutsideIn(X): modular type inference with local assumptions. J. Funct. Program. 21(4–5), 333–412 (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Gelain, A., Vasconcellos, C., Camarão, C., Ribeiro, R. (2015). Type Inference for GADTs and Anti-unification. In: Pardo, A., Swierstra, S. (eds) Programming Languages. SBLP 2015. Lecture Notes in Computer Science(), vol 9325. Springer, Cham. https://doi.org/10.1007/978-3-319-24012-1_2
Download citation
DOI: https://doi.org/10.1007/978-3-319-24012-1_2
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24011-4
Online ISBN: 978-3-319-24012-1
eBook Packages: Computer ScienceComputer Science (R0)