A Principled Approach to Ornamentation in ML

Abstract : Ornaments are a way to describe changes in datatype definitions reorganizing, adding, or dropping some pieces of data so that functions operating on the bare definition can be partially and sometimes totally lifted into functions operating on the ornamented structure. We propose an extension of ML with higher-order ornaments, demonstrate its expressiveness with a few typical examples, including code refactoring, study the metatheoretical properties of ornaments, and describe their elaboration process. We formalize ornamentation via an a posteriori abstraction of the bare code, called generic lifting, which lives in a meta-language above ML. The lifted code is obtained by application of the generic lifting to well-chosen arguments, followed by staged reduction, and some remaining simplifications. We use logical relations to closely relate the lifted code to the bare code.
Type de document :
Rapport
[Research Report] RR-9117, Inria. 2017
Liste complète des métadonnées

Littérature citée [18 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01628060
Contributeur : Thomas Williams <>
Soumis le : mardi 7 novembre 2017 - 16:36:49
Dernière modification le : jeudi 26 avril 2018 - 10:28:33
Document(s) archivé(s) le : jeudi 8 février 2018 - 12:10:25

Fichier

ornaments-long.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Thomas Williams, Didier Rémy. A Principled Approach to Ornamentation in ML. [Research Report] RR-9117, Inria. 2017. 〈hal-01628060〉

Partager

Métriques

Consultations de la notice

113

Téléchargements de fichiers

92