Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Logic/Constraint Programming and Concurrency: The Hard-Won Lessons of the Fifth Generation Computer Project Read chapter Read first chapter

2016 | OriginalPaper | Chapter

Executable Relational Specifications of Polymorphic Type Systems Using Prolog

Authors : Ki Yung Ahn, Andrea Vezzosi

Published in: Functional and Logic Programming

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

A concise, declarative, and machine executable specification of the Hindley–Milner type system (HM) can be formulated using logic programming languages such as Prolog. Modern functional language implementations such as the Glasgow Haskell Compiler support more extensive flavors of polymorphism beyond Milner’s theory of type polymorphism in the late 70’s. We progressively extend the HM specification to include more advanced type system features. An interesting development is that extending dimensions of polymorphism beyond HM resulted in a multi-staged solution: resolve the typing relations first, while delaying to resolve kinding relations, and then resolve the delayed kinding relations. Our work demonstrates that logic programing is effective for prototyping polymorphic type systems with rich features of polymorphism, and that logic programming could have been even more effective for specifying type inference if it were equipped with better theories and tools for staged resolution of different relations at different levels.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

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

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

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

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

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




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

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




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Space-Efficient Planar Acyclicity Constraints
next chapter Proof Relevant Corecursive Resolution
Footnotes
2
We intentionallay adopted the same symbol as the application operator $ in the Haskell standard library. In contrast to the right-associative operator in Haskell, our operator represents the default function application most often denoted by empty spaces and left-associative by convention.
 
3
Here, in this subsection, we consider non-recursive bindings only but the specification of HM can be easily modified to support recursive bindings (see Sect. 3.1).
 
4
See miniml.apl in the examples directory of the \(\alpha \)Prolog version 0.4 or 0.3.
 
5
Kanren is a phonetic transcription of the Kanji word meaning “relation”. See http://​kanren.​sourceforge.​net/​.
 
Literature
1.
Abel, A., Matthes, R., Uustalu, T.: Generalized iteration and coiteration for higher-order nested datatypes. In: FoSSaCS 2003 (2003)
2.
Ahn, K.Y.: The Nax language. Ph.D. thesis, Department of Computer Science, Portland State University, November 2014
3.
Ahn, K.Y., Sheard, T.: A hierarchy of Mendler-style recursion combinators. In: ICFP 2011. ACM (2011)
4.
Ahn, K.Y., Sheard, T., Fiore, M., Pitts, A.M.: System Fi: a higher-order polymorphic lambda calculus with erasable term indices. In: TLCA 2013 (2013)
5.
Alves, S., Florido, M.: Type inference using Constraint Handling Rules. In: WFLP 2001, vol. 64 of Electronic Notes in TCS, pp. 56–72. Elsevier (2002)
6.
Ancona, D., Lagorio, G.: Coinductive type systems for object-oriented languages. In: Drossopoulou, S. (ed.) ECOOP 2009. LNCS, vol. 5653, pp. 2–26. Springer, Heidelberg (2009)CrossRef
7.
Barendregt, H.: Introduction to generalized type systems. J. Funct. Program. 1(2), 125–154 (1991)MathSciNetMATH
8.
Bird, R., Meertens, L.: Nested datatypes. In: MPC: 4th International Conference on Mathematics of Program Construction (1998)
9.
Byrd, W.E.: Relational programming in miniKanren: techniques, applications,and implementations. Ph.D. thesis, Indiana University (2009)
10.
Cheney, J., Urban, C.: \(\alpha \)Prolog: A logic programming language with names, binding, and \(\alpha \)-equivalence. In: Demoen, B., Lifschitz, V. (eds.) ICLP 2004. LNCS, vol. 3132, pp. 269–283. Springer, Heidelberg (2004)CrossRef
11.
Csorba, J., Zombori, Z., Szeredi, P.: Pros and cons of using CHR for type inference. In: CHR 2012, KU Leuven, Deptarment of CS, Tech-report CW 624 (2012)
12.
Despeyroux, T.: Executable specification of static semantics. In: MacQueen, D.B., Plotkin, G., Kahn, G. (eds.) Semantics of Data Types 1984. LNCS, vol. 173, pp. 215–233. Springer, Heidelberg (1984)CrossRef
13.
Dubois, C.: Proving ML type soundness within Coq. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 126–144. Springer, Heidelberg (2000)CrossRef
14.
Friedman, D.P., Byrd, W.E., Kiselyov, O.: The Reasoned Schemer. MIT Press, Cambridge (2005). ISBN 978-0-262-56214-0
15.
Fu, P., Komendantskaya, E.: A type theoretic approach to structural resolution. In: Pre-Proceedings of LOPSTR 2015 (2015)
16.
Gaster, B.R., Jones, M.P.: A polymorphic type system for extensible records and variants. Technical report (1996)
17.
J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Université Paris VII (1972)
18.
Hemann, J., Friedman, D.P.: \(\mu \)Kanren: A minimal functional core for relational programming. In: Scheme 2013 (2013)
19.
Johann, P., Komendantskaya, E., Komendantskiy, V.: Structural resolution for logic programming. In: Techincal Communications of ICLP (2015)
20.
Jones, M.P.: Typing Haskell in Haskell. In: Haskell 1999, October 1999
21.
Matthes, R.: Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Ph.D. thesis, Ludwig-Maximilians University (1998)
22.
23.
Mitchell, D.J., Nadathur, G.: System description: teyjus - a compiler and abstract machine based implementation of \(\lambda \)prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)CrossRef
24.
Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theor. Pract. Object Syst. 5(1), 35–55 (1999). ISSN 1074–3227CrossRef
25.
26.
Poole, D., Mackworth, A.K.: Artificial Intelligence - Foundations of Computational Agents. Cambridge University Press, Cambridge (2010)CrossRefMATH
27.
Russo, C.V., Vytiniotis, D.: Qml: explicit first-class polymorphism for ml. In: ML 2009, pp. 3–14. ACM, New York (2009)
28.
Schrijvers, T., Costa, V.S., Wielemaker, J., Demoen, B.: Towards typed prolog. In: Garcia de la Banda, M., Pontelli, E. (eds.) ICLP 2008. LNCS, vol. 5366, pp. 693–697. Springer, Heidelberg (2008)CrossRef
29.
Schrijvers, T., Demoen, B., Desouter, B., Wielemaker, J.: Delimited continuations for prolog. In: Proceedings of ICLP 2013 TPLP (2013)
30.
Scott, D.S.: A type-theoretic alternative to CUCH ISWIM OWHY. Manuscript (1969)
31.
SWI-Prolog team. SWI-Prolog reference manual (section 4.2) (2005)
32.
Urban, C., Nipkow, T.: Nominal verification of algorithm W. In: From Semantics to Computer Science, pp. 363–382. Cambridge University Press (2009)
33.
Vene, V.: Categorical Programming with Inductive and Coinductive Types. Ph.D. thesis, Department of Computer Science, University of Tartu, August 2000
34.
Yorgey, B.A., Weirich, S., Cretin, J., Peyton Jones, S., Vytiniotis, D., Magalhães, J.P.: Giving Haskell a promotion. In: TLDI 2012. ACM (2012)
Metadata
Title
Executable Relational Specifications of Polymorphic Type Systems Using Prolog
Authors
Ki Yung Ahn
Andrea Vezzosi
Copyright Year
2016
Book
Functional and Logic Programming

Print ISBN: 978-3-319-29603-6

Electronic ISBN: 978-3-319-29604-3

Copyright Year: 2016

DOI
https://doi.org/10.1007/978-3-319-29604-3_8

Premium Partner

    Image Credits