nach oben

vorheriges Kapitel Automatic Inference of Loop Complexity Through ...

nächstes Kapitel Preserving Lexical Scoping When Dynamically Emb...

Tipp

Weitere Kapitel dieses Buchs durch Wischen aufrufen

2015 | OriginalPaper | Buchkapitel

Type Inference for GADTs and Anti-unification

Erstes Kapitel lesen

Autoren: Adelaine Gelain, Cristiano Vasconcellos, Carlos Camarão, Rodrigo Ribeiro

Verlag: Springer International Publishing

Erschienen in: Programming Languages

» Jetzt Zugang zum Volltext erhalten

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.

Bitte loggen Sie sich ein, um Zugang zu diesem Inhalt zu erhalten

Jetzt einloggen Kostenlos registrieren

Sie möchten Zugang zu diesem Inhalt erhalten? Dann informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 69.000 Bücher
über 500 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 50.000 Bücher
über 380 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Umwelt
Maschinenbau + Werkstoffe

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 58.000 Bücher
über 300 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Testen Sie jetzt 30 Tage kostenlos.

Jetzt informieren

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

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

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)

10.

Plotkin, G.D.: A note on inductive generalisation. Mach. intell. 5(1), 153–163 (1970) MATH

11.

Plotkin, G.D.: A further note on inductive generalisation. Mach. Intell. 6, 101–124 (1971) MATH

12.

Pottier, F., Régis-Gianas, Y.: Stratified type inference for generalized algebraic data types. SIGPLAN Not. 41(1), 232–244 (2006) CrossRef

13.

Ribeiro, R., Camarão, C.: Ambiguity and context-dependent overloading. J. Braz. Comput. Soc. 19(3), 313–324 (2013) MathSciNetCrossRef

14.

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

15.

Schrijvers, T., Jones, S.P., Sulzmann, M., Vytiniotis, D.: Complete and decidable type inference for GADTs. SIGPLAN Not. 44(9), 341–352 (2009) CrossRefMATH

16.

Smith, G.: Polymorphic type inference for languages with overloading and subtyping. Ph.D. thesis, Cornell University (1991)

17.

Smith, G.: Principal type schemes for functional programs with overloading and subtyping. Sci. Comput. Program. 23(2–3), 197–226 (1994) MathSciNetCrossRefMATH

18.

Stuckey, P., Sulzmann, M.: A Theory of overloading. In: Proceedings of the 7th ACM International Conference on Functional Programming, pp. 167–178 (2002)

19.

Sulzmann, M., Schrijvers, T., Stuckey, P.J.: Type Inference for GADTs via Herbrand Constraint Abduction (2008)

20.

Team, G., et al.: The Glorious Glasgow Haskell Compilation System User’s Guide, Version 7.10.1 (2015)

21.

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)

22.

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

Titel

Type Inference for GADTs and Anti-unification

Buch

Programming Languages

Print ISBN: 978-3-319-24011-4

Electronic ISBN: 978-3-319-24012-1

https://doi.org/10.1007/978-3-319-24012-1

DOI

https://doi.org/10.1007/978-3-319-24012-1_2

Autoren:

Adelaine Gelain
Cristiano Vasconcellos
Carlos Camarão
Rodrigo Ribeiro

Verlag

Springer International Publishing

Sequenznummer

Premium Partner

Bildnachweise