Portal de Periódicos da CAPES

Retrieving library identifiers via equational matching of types

1990; Springer Science+Business Media; Linguagem: Inglês

10.1007/3-540-52885-7_117

1611-3349

Mikael Rittri,

Formal Methods in Verification

In functional programming environments, one can use types as search keys in program libraries, if one disregards trivial differences in argument order or currying. A way to do this is to identify types that are isomorphic in every Cartesian closed category; simpler put, types should be identified if they are equal under an arithmetic interpretation, with Cartesian product as multiplication and function space as exponentiation. When the type system is polymorphic, one may also want to retrieve identifiers of types more general than the query. This paper describes a method to do both, that is, an algorithm for pattern matching modulo canonical CCC-isomorphism. The algorithm returns a finite complete set of matchers. An implementation shows that satisfactory speed can be achieved for library search.