×

Using types as search keys in function libraries. (English) Zbl 1155.68452

Summary: A 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.

MSC:

68Q65 Abstract data types; algebraic specification
68Q55 Semantics in the theory of computing
68N18 Functional programming and lambda calculus
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] DOI: 10.1016/S0747-7171(89)80022-7 · Zbl 0691.03003 · doi:10.1016/S0747-7171(89)80022-7
[2] DOI: 10.1145/322217.322225 · Zbl 0452.68050 · doi:10.1145/322217.322225
[3] DOI: 10.1007/BFb0095664 · doi:10.1007/BFb0095664
[4] DOI: 10.1007/BFb0018341 · doi:10.1007/BFb0018341
[5] Lambek, H. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism pp 376– (1980)
[6] Kirchner, Centre de Recherche en Informatique (1984)
[7] Jeanrond, Lecture Notes in Computer Science 87 (1980)
[8] Huet, Combinators and Functional Programming Languages 242 (1985)
[9] DOI: 10.2307/1999575 · Zbl 0533.03015 · doi:10.2307/1999575
[10] Rittri, Lecture Notes in Artificial Intelligence 449 (1990)
[11] Plotkin, Lecture notes (1980)
[12] DOI: 10.1145/322248.322251 · Zbl 0479.68092 · doi:10.1145/322248.322251
[13] DOI: 10.1145/321662.321668 · Zbl 0237.68003 · doi:10.1145/321662.321668
[14] Harper, Introduction to Standard ML. (1986)
[15] Gurevič, Ann. of Pure and Appl. Logic. (1989)
[16] Goldblatt, Studies in Logic and the Foundation of Mathematics 98 (1979) · Zbl 0434.03050
[17] DOI: 10.1016/0304-3975(76)90085-2 · Zbl 0368.02028 · doi:10.1016/0304-3975(76)90085-2
[18] Turner, Functional Programming Languages and Computer Architecture 201 pp 1– (1985) · doi:10.1007/3-540-15975-4_26
[19] DOI: 10.1007/BF01084396 · Zbl 0509.18002 · doi:10.1007/BF01084396
[20] DOI: 10.1093/comjnl/32.2.127 · doi:10.1093/comjnl/32.2.127
[21] DOI: 10.1016/S0747-7171(89)80012-4 · Zbl 0678.68098 · doi:10.1016/S0747-7171(89)80012-4
[22] Augustsson, Lazy ML User’s Manual (1988)
[23] Martin, Notices of Am. Math. Soc. 19 pp 778– (1972)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.