Using types as search keys in function libraries

Journal of Functional Programming - Tập 1 Số 1 - Trang 71-89 - 1991
Mikael Rittri1
1Department of Computer Sciences, Chalmers University of Technology and University of Göteborg, Sweden

Tóm tắt

AbstractA method is proposed to search for an identifier in a functional program library by using its Hindley–Milner type as a key. This can be seen as an approximation of using the specification as a key.Functions that only differ in their argument order or currying are essentially the same, which is expressed by a congruence relation on types. During a library search, congruent types are identified. If a programmer is not satisfied with the type of a found value, he can use a conversion function (like curry), which must exist between congruent types, to convert the value into the type of his choice.Types are congruent if they are isomorphic in all cartesian closed categories. To put it more simply, types are congruent if they are equal under an arithmetical interpretation, with cartesian product as multiplication and function space as exponentiation. This congruence relation is characterized by seven equational axioms. There is a simple term-rewriting algorithm to decide congruence, using which a search system has been implemented for the functional language Lazy ML, with good performance.The congruence relation can also be used as a basis for other search strategies, e.g. searching for identifiers of a more general type, modulo congruence or allowing free type variables in queries.

Từ khóa


Tài liệu tham khảo

Uddeborg G. O. 1988. A functional parser generator. Licentiate thesis, Dept. of Comp. Sci., Chalmers Univ. of Tech., S-412 96 Göteborg, Sweden. Also as PMG Report 43 (without source code).

10.1007/3-540-15975-4_26

10.1007/BF01084396

10.1016/S0747-7171(89)80012-4

10.1145/322217.322225

Gonnet G. H. 1984. Determining the equivalence of expressions in random polynomial time. In 16th ACM Symp. on the Theory of Computing, Washington DC.

Martin, 1972, Axiomatic bases for equational theories of natural numbers, Notices of Am. Math. Soc., 19, 778

Jeanrond, 1980, Lecture Notes in Computer Science, 87

10.1007/BFb0018341

10.1093/comjnl/32.2.127

Narendran P. , Pfenning F. and Statman R. 1989. On the unification problem for cartesian closed categories. Addresses: P. Narendran, State Univ. of New York at Albany, USA. F. Pfenning and R. Statman Carnegie Mellon Univ., Pittsburgh, USA. E-mail: [email protected], [email protected], [email protected].

Goldblatt, 1979, Studies in Logic and the Foundation of Mathematics, 98

Damas L. and Milner R. 1982. Principal type-schemes for functional programs. In 9th ACM Symp. on Principles of Programming Languages.

10.1145/321662.321668

Augustsson, 1988, Lazy ML User's Manual

Bruce K. B. and Longo G. 1985. Provable isomorphisms and domain equations in models of typed languages (preliminary version). In 17th ACM Symp. on the Theory of Computing, Providence.

Gurevič, 1989, Equational theory of positive numbers with exponentiation is not finitely axiomatizable, Ann. of Pure and Appl. Logic.

Lambek, 1980, H. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 376

Plotkin, 1980, Lecture notes

10.1016/0304-3975(76)90085-2

Harper, 1986, Introduction to Standard ML.

Rittri M. 1990 b. Searching Program Libraries by Type and Proving Compiler Correctness by Bisimulation. PhD thesis, Dept. of Comp. Sci., Chalmers Univ. of Tech. and Univ. of Göteborg, S-412 96 Göteborg, Sweden. E-mail: [email protected].

Henson, 1984, Some applications of Nevanlinna theory to mathematical logic: Identities of exponential functions, Trans. of Am. Math. Soc., 282, 1

Huet, 1985, Combinators and Functional Programming Languages, 242

Kirchner, 1984, Centre de Recherche en Informatique

Kirchner C. 1985. Méthodes et outils de conception systématique d'algorithmes d'unification dans les théories équationelles. PhD thesis, Université de Nancy I, France. E-mail: [email protected].

Lang B. 1978. Matching with multiplication and exponentiation (May). Author's current address: INRIA, Domaine de Voluceau, Rocquencourt, B.P. 105, F-78153 Le Chesnay Cedex, France. E-mail: [email protected].

10.1007/BFb0095664

PMG Memo 69, Dept. of Comp. Sci., Chalmers Univ. of Tech., S-412 96 Göteborg, Sweden. Email: [email protected].

Martin C. F. 1973. Equational Theories of Natural Numbers and Transfinite Ordinals. PhD thesis, Univ. of California, Berkeley, CA 94720, USA. The relevant results appear also in Martin (1972).

10.1145/322248.322251

Rittri M. 1989. lmlseek – a program to search for identifiers in LML programs by type (July).

Rittri, 1990, Lecture Notes in Artificial Intelligence, 449

10.1016/S0747-7171(89)80022-7

Runciman C. and Toyn I. 1989. Retrieving re-usable software components by polymorphic type. In 4th Int. Conf. on Functional Programming Languages and Computer Architecture, London, UK.,ACM Press, Addison-Wesley.

Thông tin
Thông tin xuất bản

Journal of Functional Programming

Tập 1 Số 1

71-89

Thông tin tác giả