Bridging Curry and Church's typing style
Abstract
There are two versions of type assignment in the -calculus: Church-style, in which the type of each variable is fixed, and Curry-style (also called domain free), in which it is not. As an example, in Church-style typing, x:A.x is the identity function on type A, and it has type AA but not BB for a type B different from A. In Curry-style typing, x.x is a general identity function with type CC for every type C. In this paper, we will show how to interpret in a Curry-style system every Pure Type System (PTS) in the Church-style without losing any typing information. We will also prove a kind of conservative extension result for this interpretation, a result which implies that for most consistent PTSs of the Church-style, the corresponding Curry-style system is consistent. We will then show how to interpret in a system of the Church-style (a modified PTS, stronger than a PTS) every PTS-like system in the Curry style.
References
[1]
H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, North-Holland, 1984.
[2]
H.P. Barendregt, Lambda calculi with types, in: Handbook of Logic in Computer Science, vol. 2, Oxford University Press, 1992, pp. 117-309.
[3]
G. Barthe, M. Sorensen, Domain free pure type systems, J. Funct. Program., 10 (2000) 417-452.
[4]
M. Bunder, W. Dekkers, Pure type systems with more liberal rules, J. Symb. Log., 66 (2001) 1561-1580.
[5]
A. Church, A formulation of the simple theory of types, J. Symb. Log., 5 (1940) 56-68.
[6]
T. Coquand, G. Huet, The calculus of constructions, Inf. Comput., 76 (1988) 95-120.
[7]
H. Curry, J. Hindley, J. Seldin, Combinatory Logic, North-Holland Publishing Company, Amsterdam, London, 1972.
[8]
J.-Y. Girard, Interprétation fonctionelle et élimination des coupures dans l'arithmétique d'ordre supérieur, Université Paris 7, 1972.
[9]
J. Hindley, J. Seldin, Lambda-Calculus and Combinators, An Introduction, Cambridge University Press, 2008.
[10]
W.A. Howard, The formulas-as-types notion of construction, in: To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, New York, 1980, pp. 479-490.
[11]
Fairouz Kamareddine, Twan Laan, Rob Nederpelt, Refining the Barendregt cube using parameters, in: Lecture Notes in Computer Science, vol. 2024, Springer, 2001, pp. 375-389.
[12]
Fairouz Kamareddine, Twan Laan, Rob Nederpelt, A Modern Perspective on Type Theory from Its Origins Until Today, Kluwer Academic Publishers, May 2004.
[13]
Marc Bezem, J.W. Klop, Roel de Vrijer, Term Rewriting Systems, Cambridge University Press, 2003.
[14]
Z. Luo, ECC, an extended calculus of constructions, in: Proceedings of the Fourth Annual Symposium on Logic in Computer Science, 1989.
[15]
Z. Luo, An extended calculus of constructions, University of Edinburgh, 1990.
[16]
G. Pottinger, Ulysses: logical and computational foundations of the primitive inference engine, ORA Corporation, January 1988.
[17]
G. Pottinger, A tour of the multivariate lambda calculus, in: Truth or Consequences: Essays in Honor of Nuel Belnap, Kluwer Academic Publishers, Dordrecht, Boston, London, 1990, pp. 209-229.
[18]
G. Pottinger, J.P. Seldin, Interpreting Church-style typed λ-calculus in Curry-style type assignment. Former title, "Note on ¿-Reduction and Labelling Bound Variables in Typed λ-Calculus," unpublished.
[19]
J.C. Reynolds, Towards a Theory of Type Structure, Springer-Verlag, 1974.
[20]
J. Seldin, Progress report on generalized functionality, Ann. Math. Log., 17 (1979) 29-59.
[21]
J. Seldin, On the relation between Church-style typing and Curry-style typing, unpublished.
[22]
S. van Bakel, L. Liquori, S.R. della Rocca, P. Urzyczyn, Comparing cubes of typed and type assignment systems, Ann. Pure Appl. Logic, 86 (1997) 267-303.
- Bridging Curry and Church's typing style
Recommendations
A church-style intermediate language for MLF
MLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during ...
Partially Typed Terms between Church-Style and Curry-Style
TCS '00: Proceedings of the International Conference IFIP on Theoretical Computer Science, Exploring New Frontiers of Theoretical InformaticsWe introduce several structures between Church-style and Curry-style based on partially typed terms formalism. In the uniform framework, we study the static properties of the λ-terms between the two styles. It is proved that type checking, typability, ...
A church-style intermediate language for MLF
FLOPS'10: Proceedings of the 10th international conference on Functional and Logic ProgrammingMLF is a type system that seamlessly merges ML-style implicit but second-class polymorphism with System-F explicit first-class polymorphism. We present xMLF, a Church-style version of MLF with full type information that can easily be maintained during ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Copyright © Elsevier B.V.
Publisher
Elsevier Science Publishers B. V.
Netherlands
Publication History
Published: 01 November 2016
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 13 Dec 2024