{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:57:30Z","timestamp":1776891450115,"version":"3.51.2"},"reference-count":42,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2017,2,6]],"date-time":"2017-02-06T00:00:00Z","timestamp":1486339200000},"content-version":"unspecified","delay-in-days":36,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2017]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    Functional programmers from all horizons strive to use, and sometimes abuse, their favorite type system in order to capture the invariants of their programs. A widely used tool in that trade consists in defining finely indexed datatypes. Operationally, these types\n                    <jats:italic>classify<\/jats:italic>\n                    the programmer's data, following the ML tradition. Logically, these types\n                    <jats:italic>enforce<\/jats:italic>\n                    the program invariants in a novel manner. This new programming pattern, by which one programs\n                    <jats:italic>over<\/jats:italic>\n                    inductive definitions to account for some invariants, lead to the development of a theory of ornaments (McBride, 2011\n                    <jats:italic>Ornamental Algebras, Algebraic Ornaments<\/jats:italic>\n                    . Unpublished). However, ornaments originate as a dependently-typed object and may thus appear rather daunting to a functional programmer of the non-dependent kind. This article aims at presenting ornaments\n                    <jats:italic>from first-principles<\/jats:italic>\n                    and, in particular, to declutter their presentation from syntactic considerations. To do so, we shall give a sufficiently abstract model of indexed datatypes by means of many-sorted signatures. In this process, we formalize our intuition that an indexed datatype is the combination of a data-\n                    <jats:italic>structure<\/jats:italic>\n                    and a data-\n                    <jats:italic>logic<\/jats:italic>\n                    . Over this abstraction of datatypes, we shall recast the definition of ornaments, effectively giving a model of ornaments. Benefiting both from the operational\n                    <jats:italic>and<\/jats:italic>\n                    abstract nature of many-sorted signatures, ornaments should appear applicable and, one hopes, of interest beyond the type-theoretic circles, case in point being languages with generalized abstract datatypes or refinement types.\n                  <\/jats:p>","DOI":"10.1017\/s0956796816000356","type":"journal-article","created":{"date-parts":[[2017,2,5]],"date-time":"2017-02-05T23:23:45Z","timestamp":1486337025000},"source":"Crossref","is-referenced-by-count":8,"title":["The essence of ornaments"],"prefix":"10.46298","volume":"27","author":[{"given":"PIERRE-EVARISTE","family":"DAGAND","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2017,2,6]]},"reference":[{"key":"S0956796816000356_ref20","unstructured":"Guibas L. J. & Sedgewick R. (1978) A dichromatic framework for balanced trees. In Foundations of Computer Science, pp. 8\u201321."},{"key":"S0956796816000356_ref25","unstructured":"Ko H.-S. (2014) Analysis and Synthesis of Inductive Families. PhD Thesis, University of Oxford."},{"key":"S0956796816000356_ref39","first-page":"158","volume-title":"Central European Functional Programming School","author":"Sheard","year":"2007"},{"key":"S0956796816000356_ref9","unstructured":"Coq development team. (2015) The Coq proof assistant reference manual."},{"key":"S0956796816000356_ref14","first-page":"268","volume-title":"Programming Language Design and Implementation","author":"Freeman","year":"1991"},{"key":"S0956796816000356_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004112000394"},{"key":"S0956796816000356_ref15","unstructured":"Fumex C. (2012) Induction and Coinduction Schemes in Category Theory. PhD Thesis, University of Strathclyde."},{"key":"S0956796816000356_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100061284"},{"key":"S0956796816000356_ref32","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054109006462"},{"key":"S0956796816000356_ref28","volume-title":"Intuitionistic Type Theory","author":"Martin-L\u00f6f","year":"1984"},{"key":"S0956796816000356_ref34","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511530104"},{"key":"S0956796816000356_ref3","first-page":"263","article-title":"An algorithm for the organization of information","volume":"146","author":"Adelson-Velskii","year":"1962","journal-title":"Dokl. Akad. Nauk USSR"},{"key":"S0956796816000356_ref2","first-page":"1","article-title":"\u2202 for data: Differentiating data structures","volume":"65","author":"Abbott","year":"2005","journal-title":"Fundam. Inform."},{"key":"S0956796816000356_ref22","unstructured":"Hinze R. (1998) Numerical Representations as Higher-Order Nested Datatypes. Technical Report, Institut f\u00fcr Informatik III, Universit\u00e4t Bonn."},{"key":"S0956796816000356_ref11","unstructured":"Dagand P.-E. & McBride C. (2013) A categorical treatment of ornaments. Logics Comput. Sci. 530\u2013539."},{"key":"S0956796816000356_ref1","doi-asserted-by":"crossref","unstructured":"Abbott M. (2003) Categories of Containers. Ph.D. thesis, University of Leicester.","DOI":"10.1007\/3-540-36576-1_2"},{"key":"S0956796816000356_ref7","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/9153.001.0001","volume-title":"Certified Programming with Dependent Types","author":"Chlipala","year":"2013"},{"key":"S0956796816000356_ref12","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211308"},{"key":"S0956796816000356_ref27","unstructured":"Ko H.-S. & Gibbons J. (2013) Relational algebraic ornaments. In Workshop on Dependently-Typed Programming, pp. 37\u201348."},{"key":"S0956796816000356_ref4","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:9)2012"},{"key":"S0956796816000356_ref40","first-page":"761","article-title":"The category-theoretic solution of recursive domain equations","volume":"11","author":"Smyth","year":"1982","journal-title":"Foundations of Computer Science"},{"key":"S0956796816000356_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00145-4"},{"key":"S0956796816000356_ref41","doi-asserted-by":"crossref","unstructured":"Swamy N. , Chen J. , Fournet C. , Strub P.-Y. , Bhargavan K. & Yang J. (2011) Secure distributed programming with value-dependent types. In Proceedings of International Conference on Functional Programming, ACM, pp. 266\u2013278.","DOI":"10.1145\/2034773.2034811"},{"key":"S0956796816000356_ref23","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002864"},{"key":"S0956796816000356_ref6","unstructured":"Cheney J. & Hinze R. (2003) First-Class Phantom Types. Technical Report, Cornell University."},{"key":"S0956796816000356_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24849-1_14"},{"key":"S0956796816000356_ref21","unstructured":"Hamana M. & Fiore M. (2011) A foundation for GADTs and inductive families: Dependent polynomial functor approach. In Workshop on Generic Programming, pp. 59\u201370."},{"key":"S0956796816000356_ref31","unstructured":"Morris P. & Altenkirch T. (2009) Indexed containers. Logics Comput. Sci. pp. 277\u2013285."},{"key":"S0956796816000356_ref10","first-page":"103","volume-title":"Proceedings of International Conference on Functional Programming","author":"Dagand","year":"2012"},{"key":"S0956796816000356_ref26","unstructured":"Ko H.-S. & Gibbons J. (2011) Modularising inductive families. In Workshop on Generic Programming, pp. 13\u201324."},{"key":"S0956796816000356_ref37","doi-asserted-by":"crossref","unstructured":"Schrijvers T. , Peyton Jones S. , Sulzmann M. & Vytiniotis D. (2009) Complete and decidable type inference for GADTs. In Proceedings of International Conference on Functional Programming, Edinburgh, Scotland: ACM, pp. 341\u2013352.","DOI":"10.1145\/1596550.1596599"},{"key":"S0956796816000356_ref8","volume-title":"Implementing Mathematics with the Nuprl Proof Development System","author":"Constable","year":"1986"},{"key":"S0956796816000356_ref29","unstructured":"McBride C. (2011) Ornamental Algebras, Algebraic Ornaments. Unpublished."},{"key":"S0956796816000356_ref35","doi-asserted-by":"crossref","unstructured":"Petersson K. & Synek D. (1989) A set constructor for inductive sets in Martin-L\u00f6f's type theory. In Category Theory and Computer Science, pp. 128\u2013140.","DOI":"10.1007\/BFb0018349"},{"key":"S0956796816000356_ref33","unstructured":"Norell U. (2007) Towards a Practical Programming Language Based on Dependent Type Theory. PhD Thesis, Chalmers University of Technology."},{"key":"S0956796816000356_ref42","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1145\/2633628.2633631","volume-title":"Workshop on Generic Programming","author":"Williams","year":"2014"},{"key":"S0956796816000356_ref24","volume-title":"The Art of Computer Programming, Volume II: Seminumerical Algorithms","author":"Knuth","year":"1981"},{"key":"S0956796816000356_ref19","unstructured":"Goguen J. A. , Thatcher J. W. , Wagner E. G. & Wright J. B. (1975 May) Abstract data-types as initial algebras and correctness of data representations. In Proceedings of the Conference on Computer Graphics, Pattern Recognition and Data Structure."},{"key":"S0956796816000356_ref30","unstructured":"Morris P. (2007) Constructing Universes for Generic Programming. PhD Thesis, University of Nottingham."},{"key":"S0956796816000356_ref18","first-page":"198","volume-title":"Workshop on Logical Environments","author":"Goguen","year":"1993"},{"key":"S0956796816000356_ref5","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681300018X"},{"key":"S0956796816000356_ref36","first-page":"232","volume-title":"Principles of Programming Languages","author":"Pottier","year":"2006"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796816000356","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:19:53Z","timestamp":1776889193000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796816000356\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"references-count":42,"alternative-id":["S0956796816000356"],"URL":"https:\/\/doi.org\/10.1017\/s0956796816000356","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]},"article-number":"e9"}}