Isomorphisms are back!: Smart indexing for function retrieval by unification modulo type isomorphisms

Autor: Allain, Clément, Radanne, Gabriel, Gonnord, Laure
Přispěvatelé: Laboratoire de l'Informatique du Parallélisme (LIP), École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), CASH - Compilation and Analysis, Software and Hardware (CASH), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire de l'Informatique du Parallélisme (LIP), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure de Lyon (ENS de Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Centre National de la Recherche Scientifique (CNRS), ANR-17-CE23-0004,CODAS,Ordonnancement de programmes à structures de données complexes(2017), École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Lyon (ENS Lyon)-Université Claude Bernard Lyon 1 (UCBL), Université de Lyon-Université de Lyon-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Zdroj: ML 2021-ML Workshop
ML 2021-ML Workshop, Aug 2021, Virtual, France. pp.1-3
Popis: International audience; Sometimes, we need a function so deeply that we have to go out and search for it. How do we find it ? Sometimes, we have clues: a function which manipulates list is probably in the Listmodule. . . but not always! Sometimes, all we have is its functionality: doing the sum of a list of integers. Unfortunately, search by functionality is difficult. Rittri [1] proposed an approximation: use the type of the function as a key to search through libraries: in our case, int list->int. To avoid stumbling over details such as the order of arguments, he proposed to use matching modulo type isomorphism – a notion broader than syntactic equality. Unfortunately, algorithms for unification modulo type isomorphisms are extremely costly. Doing an exhaustive search over the whole ML ecosystem was possible at the time (with a standard library of 294 functions), but is certainly not possible anymore for the OCaml ecosystem, with 3259 opam packages, each containing several hundreds or thousands of functions.
Databáze: OpenAIRE