A Principled Approach to Ornamentation in ML - Archive ouverte HAL Access content directly
Journal Articles Proceedings of the ACM on Programming Languages Year : 2018

A Principled Approach to Ornamentation in ML

(1) , (1)
1

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 metatheoreti-cal properties of ornaments, and describe their elaboration process. We formalize ornamentation via an a poste-riori abstraction of the bare code, returning a generic term, which lives in a metalanguage above ML. The lifted code is obtained by application of the generic term 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.
Fichier principal
Vignette du fichier
ornaments-popl18-final.pdf (387.79 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-01666104 , version 1 (18-12-2017)

Identifiers

Cite

Thomas Williams, Didier Rémy. A Principled Approach to Ornamentation in ML. Proceedings of the ACM on Programming Languages, 2018, pp.1-30. ⟨10.1145/3158109⟩. ⟨hal-01666104⟩

Collections

INRIA INRIA2
535 View
904 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More