Pierre-Évariste Dagand
email: pierre-evariste.dagand@inria.fr

Inria Conor Mcbride

Under consideration for publication in J. Functional Programming 1 Transporting Functions across Ornaments

Programming with dependent types is a blessing and a curse. It is a blessing to be able to bake invariants into the definition of datatypes: we can finally write correct-by-construction software. However, this extreme accuracy is also a curse: a datatype is the combination of a structuring medium together with a special purpose logic. These domain-specific logics hamper any attempt to reuse code across similarly structured data.

In this article, we capitalise on the structural invariants of datatypes. To do so, we first adapt the notion of ornament to our universe of inductive families. We then show how code reuse can be achieved by ornamenting functions. Using these functional ornaments, we capture the relationship between functions such as the addition of natural numbers and the concatenation of lists. With this knowledge, we demonstrate how the implementation of the former informs the implementation of the latter: the user can ask the definition of addition to be lifted to lists and she will only be asked the details necessary to carry on adding lists rather than numbers.

Our presentation is formalised in a type theory with a universe of datatypes and all our constructions have been implemented as generic programs, requiring no extension to the type theory.

Introduction

Imagine designing a library for an ML-like language. For instance, we start with natural numbers and their operations, then we move to binary trees, then rose trees, etc. It is the garden of Eden: datatypes are data-structures, each coming with its unique and optimised set of operations. If we move to a language with richer datatypes, such as a dependentlytyped language, we enter the Augean stables. Where we used to have binary trees, now we have complete binary trees, red-black trees, AVL trees, and countless other variants. Worse, we have to duplicate code across these tree-like datatypes: because they are defined upon this common binarily branching structure, a lot of computationally identical operations will have to be duplicated for the type checker to be satisfied.

Since their first introduction in ML, datatypes have evolved: besides providing an organising structure for computation, they are now offering more control over what is a valid result. With richer datatypes, we can enforce invariants on top of the data-structures. In such a system, programmers strive to express the correctness of their programs in the types: a well-typed program is correct by construction.

Functional ornaments!

Whilst we have a good handle on the transformation of individual datatypes, we are still facing a major reusability issue: a datatype often comes equipped with a set of operations. Ornamenting this datatype, we have to entirely re-implement many similar operations. For example, the datatype Nat comes with operations such as addition and subtraction. When defining lists as an ornament of natural numbers, it seems natural to transport the structurepreserving functions of Nat to List A, such as moving from addition of natural numbers to concatenation of lists: More interestingly, the function we start with may involve several datatypes, each of which may be ornamented differently. In this paper, we develop the notion of functional ornament as a generalisation of ornaments to functions:

• We manually transport the comparison of numbers to the list lookup function in Section 2. This example provides the impetus for the rest of this article: we aim at explaining the structure behind it, generalise, and automate it; • For this article to be self-contained, we recall the type theoretic foundations [START_REF] Chapman | The gentle art of levitation[END_REF] upon which this article builds in Section 3. We strive to provide an intuition for our universe-based presentation of datatypes, and describe a convenient notation for inductive definitions; • We adapt ornaments to our universe of datatypes in Section 4. This presentation benefits greatly from our ability to inspect indices when defining datatypes. This allows us to consider ornaments that delete information, yielding a key simplification in the construction of the algebraic ornament from the ornamental algebra; • We describe how functions can be transported through functional ornaments. We formalise the concept of functional ornament by a universe construction in Section 5.

Based on this universe, we establish the connection between a base function (such as addition and subtraction) and its ornamented version (such as, respectively, -++and drop). Within this framework, we redevelop the example of Section 2 with all the automation offered by our framework; • In Section 6, we provide further support to drive the computer into lifting functions.

As we can see from our examples above, the lifted functions often follow the same recursion pattern and return similar constructors: with a few smart constructors, we shall remove further clutter from our libraries.

This article is an exercise in constructive mathematics: upon identifying an isomorphism, we shall look at it with our constructive glasses and obtain an effective procedure to cross it. It is crucial to note that this article is built entirely within type theory. No change or adaptation to the meta-theory is required. In particular, the validity of our constructions is justified by mere type checking. 1.5 Remark (Notations). We shall write our code in a syntax inspired by the Epigram programming language (McBride & McKinna, 2004). For an optimal experience, we recommend reading the colour version of this article, available on Dagand's webpage. Colours are used to classify the terms of the type theory. We also make use of the by ( ⇐ ) and return ( → ) programming gadgets, further extending them to account for the automatic lifting of functions. For brevity, we write pattern-matching definitions when the recursion pattern is evident and unremarkable.

As in ML, unbound variables in type signatures are universally quantified, further abating syntactic noise. For higher-order functions, we indicate the implicit arguments with the quantifier ∀ x. (. . .) -or its annotated variant ∀ x : T . (. . .) -as follows:

example (op : ∀ n. Vec A n → 1) (xs : Vec A k) (ys : Vec A l) : op xs = op ys • • • Because we implicitly quantify over unbound type variables, these variables are not explicitly bound in the definition. We rely on the convention that these implicit arguments Functional Ornaments 5 are automatically in scope of the definition, using the same variable name. For example, in the following definition, n is universally quantified in the type declaration and is in scope in the definition of lengthVec: lengthVec (vs :

Vec A n) : Nat lengthVec vs → n
The syntax of datatype definitions draws upon the ML tradition as well: its novelty will be presented by way of examples in Section 3. Following mathematical usage, we shall extensively use mixfix operators, i.e. operators in prefix, infix, postfix, or closed form.

All the constructions presented in this article have been modelled in Agda, using only standard inductive definitions and two levels of universes. Rather than commenting the machine-checked code, we have chosen to use an high-level notation. This notation relies on the reader's ability to cope with ambiguity. We shall therefore indulge in many abuse of language, as is common in mathematics. This allows us to focus on conveying ideas to the reader, rather than on satisfying a type checker. Throughout this article, we relate the high-level definitions to their Agda counterparts using a MODEL footnote indicating their location. For an absolutely formal treatment, we therefore refer the reader to the companion formalisation. The formalisation is available on Dagand's website.

♦

A shorter version of this article has appeared in the proceedings of ICFP 2012 [START_REF] Dagand | Transporting functions across ornaments[END_REF]. This version benefits from several presentational modifications to include significantly more examples (in particular, in Section 3 and Section 4). The running example -lifting the comparison function of natural numbers -is also complemented by another example, lifting the addition of natural numbers. Worked out examples, throughout the paper, shall help the reader build a strong intuition of the generic constructions at play. We have also extended the original paper with new material. In Section 4.2, we cast the forcing and detagging transformations of [START_REF] Brady | Inductive families need not store their indices. Types for proofs and programs[END_REF] in our universe of datatypes. Using these intuitions, we have streamlined the definition of reornaments and discuss the limits of iterating reornaments (Section 4.5). We have extended the lifting of recursion patterns to handle induction and case analysis (Section 6). Our treatment of the lifting of constructors (Section 6) has also treated in more details and its underlying mechanisms has been thoroughly illustrated.

From Comparison to Lookup, Manually

There is an astonishing resemblance between the comparison function -<on numbers and the list lookup function (Fig. 1). Interestingly, the similarity is not merely at the level of types. It is also in their implementation: their definition follows the same pattern of recursion (first, case analysis on the second argument; then induction on the first argument) and they both return a failure value (respectively, false and nothing) in the first case analysis and a success value (respectively, true and just) in the base case of the induction.

This raises the question: what exactly is the relation between -<and lookup? Also, could we use the implementation of -<to guide the construction of lookup? First, let us work out the relation at the type level. To this end, we use ornaments to explain how Note that the first argument is ornamented to itself, or put differently, it has been ornamented by the identity ornament idO (Definition 4.9, p.22).

Each of these ornaments come with a forgetful map:

length (as : List A) : Nat length nil → 0 length (cons a as) → suc (length as) isJust (m : Maybe A) : Bool isJust nothing → false isJust (just a)

→ true

As we shall see in Section 4.3, the forgetful maps can be automatically derived from the ornament definition.

Using these forgetful maps we deduce a relation, at the operational level, between -<and lookup. This relation is uniquely determined by the ornamentation of the individual datatypes. This coherence property is expressed as follows (n : Nat)(xs : List A) → isJust (lookup n xs) = n < length xs or, equivalently, using a commuting diagram:

Nat × List A Maybe A Nat × Nat Bool -< - lookup id × length isJust
2.1 Remark (Vocabulary). We call the function we start with the base function (here, -< -), its type being the base type (here, Nat → Nat → Bool). The richer function type built by ornamenting the individual pieces is called the functional ornament 1 of the base 1 Note that a functional ornament is entirely determined by the ornamentation of its individual components, which we shall (unambiguously) call "a functional ornament" in Section 5.2. This follows the common usage of saying that "lists are an ornament of natural numbers", when in fact lists are the result of interpreting an ornament of natural numbers.

ZU064-05-FPR paper 13 December 2013 17:37

Functional Ornaments 7 type (here, Nat → List A → Maybe A). A function inhabiting this type is called a lifting (here, lookup). A lifting is said to be coherent if it satisfies the coherence property. ♦ 2.2 Remark (Coherence and functional ornament). It is crucial to understand that the coherence of a lifting is relative to a given functional ornament: the same base function ornamented differently would give rise to a different coherence property.

For example, the base type Nat → Nat → Nat can be functionally ornamented to

Nat → List A → List A
for which drop is a coherent solution with respect to ---. However, it can also be functionally ornamented to

List A → List A → List A
for which -++is a coherent solution with respect to -+ -. Nonetheless, the two solutions are exclusive: drop is not coherent with respect to -+ -, nor is -++coherent with respect to ---. ♦

We now have a better grasp of the relation between the base function and its lifting. However, lookup remains to be implemented while making sure that it satisfies the coherence property. Traditionally, one would stop here: we would implement lookup and prove the coherence as a theorem. This works rather well in a system like Coq since it offers a powerful theorem proving environment. It does not work so well in a system like Agda that does not offer tactics to its users, forcing them to write explicit proof terms. It would not work at all in an ML language with GADTs, which has no notion of proof.

Historically, Coq has been designed for the verification of (simply-typed) programs through (dependently-typed) propositions [START_REF] Paulin-Mohring | Extraction de programmes dans le Calcul des Constructions[END_REF]. This paradigm started shifting with languages such as Epigram, Cayenne, or Agda: these systems offer an environment for dependently-typed programming. In this setting, the approach that consists in writing a simply-typed programming to prove it correct after the fact feels utterly laborious. If we have dependent types, why should we use them only for proofs, as an afterthought? A dependently-typed programming environment lets us write a lookup function correct by construction: by implementing a more finely indexed version of lookup, the user drives the type checker into verifying the necessary invariants. This article is an exploration of this paradigm, in which we develop techniques to relieve the dependently-typed programmer from the burden of proofs.

To get the computer to work for us, we would rather implement the function ilookup ilookup (m : Nat) (vs : 2.3 Remark. We overload the constructors of Maybe and IMaybe: for a bi-directional type checker, there is no ambiguity as constructors are checked against their type. ♦

Vec A n) : IMaybe A (m < n) ilookup m nil → nothing ilookup 0 (cons a vs) → just a ilookup (suc m) (cons a vs) → ilookup m vs
The rationale behind ilookup is to index the types of lookup by their unornamented version. In effect, we index the types of its arguments by the (respective) arguments m : Nat and n : Nat of -<and we index the type of its result by m < n. By doing so, we can make sure that the result computed by ilookup respects the output of -<on the unornamented indices: the result is necessarily correct, by indexing! The type of ilookup is naturally derived from the ornamentation of -<into lookup and is uniquely determined by the functional ornament we start with. We shall automate its construction in Section 5.3 with the notion of patch (Definition 5.15). (Vocabulary). Expanding further our vocabulary, such a finely indexed function that is coherent by construction is called a coherent liftings.

Remark

We had separately introduced the notion of lifting and coherence in Remark 2.1, with the idea that a lifting is not necessarily coherent. Here, we are defining the coherent lifting as those liftings that are coherent by construction. In fact, we shall establish in Theorem 5.19 that a lifting satisfying the coherence condition is isomorphic to a coherent lifting. There is therefore no ambiguity in identifying both notions of a "coherent lifting" and of a "lifting satisfying the coherence condition". ♦ [START_REF] Ko | Modularising inductive families[END_REF] use ornaments to specify the coherence requirements for functional liftings, but we work the other way around. From ilookup, we extract the lookup function

lookup (m : Nat) (xs : List A) : Maybe A lookup m xs → π 0 (forgetIMaybe (ilookup m (makeVec xs)))
and its proof of correctness

cohLookup (n : Nat) (xs : List A) : isJust (lookup n xs) = n < length xs cohLookup m xs → π 1 (forgetIMaybe (ilookup m (makeVec xs)))
where makeVec : (xs : List A) → Vec A (length xs) turns a list into a vector of the corresponding length. Operationally, it is an identity. In Section 4.4, we show that it can be automatically derived from the ornament of lists. Functional Ornaments

9

The construction of lookup and cohLookup feels automatic: we shall see in Section 5.4 how lookup can automatically be obtained by patching (Definition 5.22), while cohLookup is merely an instance of a generic coherence result (Definition 5.23). (ilookup vs. vlookup). The function ilookup is very similar to the more familiar vlookup function:

Remark

vlookup (m : Fin n) (vs : Vec A n) : A vlookup f0 (cons a xs) → a vlookup (fsuc n) (cons a xs) → vlookup n xs
These two definitions are actually equivalent, thanks to the isomorphism

(m : Nat) → IMaybe A(m < n) ∼ = Fin n → A
where we silently lift the boolean predicate m < n at the type-level, as is common practice in SSREFLECT [START_REF] Gonthier | A Small Scale Reflection Extension for the Coq system[END_REF] for instance.

Intuitively, we can move the constraint "m < n" from the result -where we return an object of type IMaybe A(m < n) -to the premise -where we expect an object of type Fin n. Indeed, we can think of the type Fin n as the combination of a number m:Nat together with a proof that m < n. ♦

With this example, we have manually unfolded the key steps of the construction of a lifting of -< -. Let us recapitulate each steps:

• Start with a base function, here -< -: Nat → Nat → Bool;

• Ornament its inductive components as desired, here Nat to ListA and Bool to MaybeA in order to describe the lifting of interest, here lookup :

Nat → List A → Maybe A satisfying (n : Nat)(xs : List A) → isJust (lookup n xs) = n < length xs
• Implement a carefully indexed version of the lifting, here

ilookup : (m : Nat)(vs : Vec A n) → IMaybe A (m < n)
• Derive the lifting, here lookup, and its coherence proof, without writing a proof! Besides, ilookup is a useful addition to our library: it corresponds to the familiar vector lookup function, a function that one would have implemented anyway. Thus, ilookup is not just some scaffolding necessary to define lookup, it is a purposeful operation on its own. This manual unfolding of the lifting is instructive: it involves many constructions on datatypes (here, the datatypes List A and Maybe A) as well as on functions (here, the type of ilookup, the definition of lookup and its coherence proof). Yet, it feels like a lot of these constructions could be automated. In Section 5, we shall build the machinery to describe these transformations and obtain them within the type theory itself.

A Universe of Datatypes

In dependently-typed systems such as Coq or Agda, datatypes are an external entity: each datatype definition extends the type theory with new introduction and elimination forms.

The validity of a datatype definition is guaranteed by a positivity-checker that is part of the meta-theory of the proof system. A consequence is that, from within the type theory, it is not possible to create or manipulate inductive definitions, since they belong to the meta-theory.

In previous work [START_REF] Chapman | The gentle art of levitation[END_REF], we have shown how to internalise inductive families into type theory. The practical outcome of this approach is that we can manipulate datatype declarations as first-class objects. We can program over the grammar of datatypes and, in particular, we can compute new datatypes from old. This is particularly useful to formalise the notion of ornament entirely within type theory. This also has a theoretical outcome: we do not need to prove meta-theoretical properties of our constructions, we can work in our type theory and use its logic as a formal system.

3.1 Remark (Theory vs. meta-theory). The constructions described in this article are also applicable in a setting where datatype definitions are not internalised: all our constructions could be justified at the meta-level and then be syntactically presented in a language, such as, say, Agda, Coq, or an ML with GADTs. Working with an internalised presentation, we can simply avoid these two levels of logic and work in the logic provided by type theory.

Our requirements on the ambient type theory are boxed in a TYPE THEORY frame (e.g., Fig. 2, p.11), whilst constructions within that type theory are boxed in a DEFINITION frame (e.g., Fig. 3,p.19). Because our work is grounded in an intensional reading of extensional isomorphisms, we box the original, extensional results in META-THEOREM frames (e.g., Equation 4.20, p.26). The proof of these results are absent from our (intensional) Agda model. Examples illustrating the various concepts are left unboxed. ♦

The type theory

Following our previous work, our requirements on the type theory are minimal: we will need Σ-types, Π-types, the unit set 1, and at least two universes, SET and SET 1 . Σ-types are denoted (a:A) × B, introduced by pairs (x, y) and eliminated by first and second projections, respectively π 0 and π 1 . Π-types are denoted (a:A) → B, introduced by λx. b and eliminated by function application. The unit set is (uniquely) inhabited by * . For convenience, we require the η-laws for the unit set, Σ-types (i.e. surjective pairing), and Π-types to hold definitionally. When x is not free in B, we use the following abbreviations:

(x : A) → B A → B (x : A) × B A × B
Hence obtaining the (non dependent) implication and conjunction from the dependent quantifiers.

For convenience, we ask for our type theory to support enumerations of tags. We shall not dwell on their type theoretic definition, which can be found elsewhere [START_REF] Dagand | Reusability and dependent types[END_REF]. We declare a (finite) enumeration of tags 'a, 'b, and 'c by writing {'a 'b 'c}. Similarly, we We also need a pre-existing notion of propositional equality, denoted -= -. We shall assume that it is reflexive, as witnessed by refl, and substitutive. Because we perform numerous pattern-matches on indexed datatypes, we also require our equality to satisfy the K rule [START_REF] Mcbride | Dependently typed functional programs and their proofs[END_REF], i.e. refl is the unique inhabitants of a propositional equality.

I) | 1 | Π (S : SET) (T : S → IDesc I) | Σ (S : SET) (T : S → IDesc I) (D : IDesc I) (X : I → SET) : SET var i X → X i 1 X → 1 Π S T X → (s : S) → T s X Σ S T X → (s : S) × T s X TYPE THEORY

Universe of descriptions

We internalise inductive families by a universe construction. The role of this universe is to describe signature functors over SET indexed by I, i.e. functors from SET I to SET I . However, up to some currying-uncurrying, this type is subject to the isomorphism

SET I → SET I (I → SET) →(I → SET) ∼ = I →(I → SET) → SET
that lets us focus on describing functors from SET I → SET, with the I-indexing being pulled away in the exponential. Following this remark, we focus first on describing signature functors of type SET I → SET (Definition 3.2). Then, to capture signature functors between slices of SET, we simply introduce an exponential (Definition 3.3), a construction akin to the Reader monad.

3.2 Definition (Universe of descriptions2 ). The universe of descriptions is defined in Fig. 2. The meaning of codes -the inhabitants of IDesc -is given by their interpretation in SET:

• Σ codes Σ-types -to build sums-of-products;

• Π codes Π-types -to capture higher-order arguments;

• 1 codes the unit type -to terminate codes;

• var codes the recursive arguments of inductive definitions, taken at an index i. Because it describes functors, this universe offers a generic map operator:

(D : func I) → : ( f : ∀ i. X i →Y i)(xs : D X i) → D Y i TYPE THEORY
Inhabitants of the func type are called descriptions. ▽

3.4 Remark (Overloaded notation). We overload the symbolto denote both the interpretation of a description code to a functor from SET I to SET (Definition 3.2), and the interpretation of a description to an endofunctor from SET I to SET I (Definition 3.3). Indeed, the latter is merely of pointwise lifting of the former. ♦ Descriptions, by interpreting to strictly positive functors on slices of SET, admit a least fixpoint4 construction:

data µ [D : func I](i : I) : SET where µ D i ∋ in (xs : D (µ D) i) TYPE THEORY
The inductive types thus formed are eliminated by a generic elimination principle5 :

induction :∀ P : ∀ i : I. µ D i → SET. (α : (i : I)(xs : D (µ D) i) → D P xs → P (in xs)) (x : µ D i) → P x TYPE THEORY
that corresponds to transfinite induction over tree-like structures. A formal description of induction can be found elsewhere [START_REF] Dagand | Reusability and dependent types[END_REF] Functional Ornaments 13 sub-trees of xs satisfy P: this captures precisely the inductive hypothesis. The argument α therefore corresponds to the inductive step: given that the induction hypothesis holds for sub-elements of xs, we must prove that P holds for the whole. In the categorical literature [START_REF] Hermida | Structural induction and coinduction in a fibrational setting[END_REF][START_REF] Fumex | Induction and coinduction schemes in category theory[END_REF], D is called the canonical lifting6 of D.

Well-founded recursive definitions by pattern-matching can be expressed in terms of the induction principle [START_REF] Dagand | of: Types for proofs and programs[END_REF]. For conciseness, we adopt a pattern-matching style when the recursive pattern is unsurprising, with the confidence that it can be expressed in terms of to induction.

Inductive definitions

Whilst we could code our inductive families directly in this universe, let us introduce an informal notation to declare datatypes. Our purpose here is to relate the reader's intuition for inductive definitions with our encodings. By relying on a more intuitive notation, we wish to make our examples more palatable. Our notation is strongly inspired by Agda's datatype declarations.

As witnessed by the Agda model, all the inductive definitions given in this article can be translated into descriptions. For a datatype T , we write T -func the code it elaborates to. Similarly, we call T -elim the elimination principle of T , and T -case the case analysis over T . These operations can be reduced generically derived from induction (McBride et al., 2004;[START_REF] Dagand | Elaborating inductive definitions[END_REF].

We also write datatype constructors (in expressions) and constructor patterns (in patternmatching clauses) using the high-level notation. In fact, they correspond to (low-level) terms built from the generic in constructor and a tuple of arguments. This elaboration mechanism is described elsewhere [START_REF] Dagand | Reusability and dependent types[END_REF].

3.5 Example. For Peano numbers (i.e. natural numbers Nat), these induction principles amount to -after suitable currying and simplification -the propositions: Nat-elim : ∀ P : Nat → SET. P 0 →((m : Nat) → P m → P (suc m)) → (n : Nat) → P n Nat-case : ∀ P : Nat → SET. P 0 →((m : Nat) → P (suc m)) → (n : Nat) → P n △ A formal presentation of the elaboration of inductive definitions to code will be found elsewhere [START_REF] Dagand | Elaborating inductive definitions[END_REF]. However, it is intuitive enough to be understood with a few examples. Three key ideas are at play:

∋ 0 | suc (o : Ord) | lim (l : Nat → Ord) Ord-func : func 1 Ord-func → λ * . Σ    '0 'suc 'lim       '0 → 1 'suc → var * 'lim → Π Nat λ -. var *   
Note the use of the higher-order Π code to express the limit ordinal.

The datatypes Bool -the Booleans 9 -and Nat -the natural numbers 10 -fall in this category too. They elaborate to descriptions indexed by 1, respectively Bool-func and Nat-func, following a similar sums-of-products pattern. We leave it as an exercise to compute their code, guided by the following remarks:

• Nat-func is a degenerate case of List-func: it is a list taking no A-argument;

• Bool-func is a degenerate case of Nat-func: it offers two constructors, but no recursive argument.

△ 3.7 Example (Indexing, following the Agda convention). Indices can be constrained to some particular value. For example, vectors can be defined by constraining the index to be

A (n = 0) ∋ nil Vec A (n = suc n ′ ) ∋ cons (n ′ : Nat)(a : A)(vs : Vec A n ′ ) Vec-func (A : SET) : func Nat Vec-func A → λn. Σ 'nil 'cons 'nil → Σ (n = 0) λ -. 1 'cons → Σ Nat λn ′ . Σ (n = suc n ′ )λ -. Σ A λ -. var n ′
The constraint notation (n =t) reads "for any index n, as long as n equals t", following the Henry Ford principle [START_REF] Mcbride | Dependently typed functional programs and their proofs[END_REF]. In particular, it must not be confused with a definition pattern-matching on the index.

In the same vein, finite sets12 can be defined by constraining the upper-bound n to always be strictly positive, and indexing the argument of fsuc by the predecessor:

data Fin (n : Nat) : SET where Fin (n = suc n ′ ) ∋ f0 (n ′ : Nat) | fsuc (n ′ : Nat)(k : Fin n ′ ) Fin-func : func Nat Fin-func → λn. Σ 'f0 'fsuc 'f0 → Σ Nat λn ′ . Σ (n = suc n ′ ) λ -. 1 'fsuc → Σ Nat λn ′ . Σ (n = suc n ′ ) λ -. var n ′ △
Note that elaboration captures the constraints on indices by using propositional equality. In the case of Vec, we first abstract over the index n, introduce the choice of constructors with the first Σ and then, once the constructors have been chosen, we restrict n to its possible value(s): 0 in the first case and suc n ′ for some n ′ in the second case. Hence the placement of the equality constraints in the elaborated code: after the constructor is chosen, we first introduce a fresh variable and then constrain the index with it. If no fresh variable needs to be introduced, we directly constrain the index.

Example (Computing over indices)

. We can also use the crucial property that a datatype definition is, in effect, a function from its indices to a choice of datatype constructors. Our notation should reflect this ability. For instance, inspired by [START_REF] Brady | Inductive families need not store their indices. Types for proofs and programs[END_REF], we give an alternative presentation of vectors that matches on the index to determine the constructor

A n ⇐ Nat-case n Vec A 0 ∋ nil Vec A (suc n) ∋ cons (a : A)(vs : Vec A n) Vec-func (A : SET) : func Nat Vec-func A n ⇐ Nat-case n Vec-func A 0 → Σ {'nil} λ -. 1 Vec-func A (suc n) → Σ {'cons} λ -. Σ A λ -. var n
In order to be fully explicit about computations, we use the "by" ( ⇐ ) gadget, which lets us appeal to any elimination principle. For simplicity, we shall use a pattern-matching style when the recursion pattern is unremarkable.

Using pattern-matching, we define the computational counterpart of finite sets by matching on n 14 , offering no constructor in the 0 case, and the two expected constructors in the suc n case:

data Fin (n : Nat) : SET where

Fin 0 ∋ Fin (suc n) ∋ f0 | fsuc (k : Fin n) Fin-func : func Nat Fin-func 0 → Σ 0 0-elim Fin-func (suc n) → Σ 'f0 'fsuc
'f0 → 1 'fsuc → var n Note the pattern used here to provide no constructor when the index is 0: we ask for a witness of the empty set, effectively preventing any constructor to be introduced. △

3.9 Remark (Forcing and detagging [START_REF] Brady | Inductive families need not store their indices. Types for proofs and programs[END_REF]). This technique of extracting information by case analysis on the indices applies to descriptions exactly where Brady's forcing and detagging optimisations apply in compilation. They eliminate just those constructors, indices and constraints which are redundant even in open computation. Detagging amounts to restricting the choice of constructors by matching on the index. For detagging to apply, constructors must be in injective correspondence with the indices. Our presentation of vectors above is obtained by detagging. By noticing whether the index is 0 or suc, we deduce the vector's constructor.

Forcing amounts to computing the argument x : X of a constructor from its index i : I. Hence, for forcing to apply, we must have a function f -ideally, the identity -from I to X ZU064-05-FPR paper 13 December 2013 17:37

Functional Ornaments

such that f i → x. Our alternative presentation of Fin above is obtained by forcing: instead of storing an index n ′ , we pattern-match on the index n and directly use its predecessor in the recursive argument. ♦

This last definition style departs radically from the one adopted by Coq, Agda, or GADTs. While it is possible to encode these definitions in Coq and Agda (through a large elimination), we have to step outside the realm of inductive definitions. Doing so, we lose access to the system's machinery for handling inductive reasoning. For instance, one would have to manually provide an elimination principle for the resulting object.

It is crucial to understand that this notation is but reflecting the actual semantics of inductive families as functors of type I →(I → SET) → SET. By using the function space I →to its full potential, we can compute over indices, not merely constrain them. With our syntax, we give the user the ability to write these functions: the reader should now understand a datatype definition as a special kind of function definition, taking indices as arguments, potentially computing over them, and eventually emitting a choice of constructors.

The original definition of ornaments was based on a universe following the Agda convention, which could only capture the indexing disciplines through equality constraints. Our ability to compute over indices has far-reaching consequences on ornaments. First, it enables the definition of a novel deletion ornament (Section 4), which uses the indexing information to delete redundant arguments in an ornamented datatype. Second, it enables a better structured and, consequently, more space-efficient definition of the algebraic ornament by the ornamental algebra (Section 4.5).

Example.

We can sensibly mix these definition styles. An example that benefits from this approach is the presentation of minimal logic15 i.e., from the other side of Curry-Howard, the simply-typed lambda calculus [START_REF] Benton | Strongly typed term representations in coq[END_REF] -given as an inductivelydefined inference system. We express the judgement Γ ⊢ T through an inductive family indexed by a context Γ of typed variables and a type T :

data (Γ : Context) ⊢ (T : Type) : SET where Γ ⊢ T ∋ var (v : T ∈ Γ) | app (S : Type)( f : Γ ⊢ S ⇒ T )(s : Γ ⊢ S) Γ ⊢ unit ∋ * Γ ⊢ S ⇒ T ∋ lam (b : Γ ; S ⊢ T )
where, for simplicity, we have restricted the language of types to the unit and the exponential:

data Type : SET where Type ∋ unit | (S : Type) ⇒ (T : Type)

data Context : SET where Context ∋ ε | (Γ : Context) ; (T : Type)
and for which we can define (inductively, in fact) a predicate T ∈ Γ that indexes a variable of type T in context Γ.

ZU064-05-FPR paper 13 December 2013 17:37 18

Dagand and McBride

Crucially, the variable and application rules take the index as is, without constraint or computation. The remaining rules depends on the index: if it is an exponential, we give the abstraction rule; if it is the unit type, we give the (only) inhabitant of that type. △ 3.11 Remark (Constraints and equality). We have been careful in using equality to introduce constraints here: our definition of datatypes is absolutely agnostic in the notion of propositional equality offered by the underlying type theory. For instance, our universe of inductive families cannot be used to define equality through the identity type: the identity type would only expose the underlying notion of equality to the user. This is unlike systems such as Coq or Agda, where propositional equality is introduced by the identity type

data Id [a 1 : A](a 2 : A) : SET where Id a 1 (a 2 = a 1 ) ∋ refl
whose elimination principle gives the J-rule [START_REF] Hofmann | The groupoid model refutes uniqueness of identity proofs[END_REF]).

In our system, this definition16 would elaborate to a description packaging the propositional equality:

Id-func (a 1 : A) : func A Id-func a 1 → λa 2 . Σ {'refl}{Σ (a 2 = a 1 ) λ -. 1} ♦ 4 A Universe of Ornaments
Originally, McBride (2013) presented the notion of ornament for a universe where the indexing discipline could only be enforced by equality constraints. As a result, the deletion ornament was not expressible in that setting. We shall now adapt the original definition to our system.

Definition (Universe of ornaments 17

). The grammar of ornaments (Fig. 3) is similar to the original one. It is defined over a base datatype D indexed by K and ornaments it to a datatype indexed by I. The (forgetful) function u : I → K specifies a refinement of the K-indices into I-indices. We can copy the base datatype (with the codes 1, Π, and Σ), extend it by inserting sets (with the code insert), and refine the indexing subject to the relation imposed by u (with the code var). Also, following Brady's insight that inductive families need not store their indices [START_REF] Brady | Inductive families need not store their indices. Types for proofs and programs[END_REF], we can delete parts of the datatype definition as long as we can provide a witness. This witness will typically be provided by the index, here in the context.

The extension of ornaments computes the description of the extended datatype. This amounts to traversing the ornament code, packing the freshly insert-ed data into Σ codes. In the delete case, no Σ code is generated: we use the witness to compute the extension of the rest of the ornament. The Π and Σ ornament codes simply duplicate the underlying

Orn D u ∋ insert (S : SET) (D + : S → Orn D u) -Refine index: Orn (var k) u ∋ var (i : u -1 k) -Copy the original: Orn 1 u ∋ 1 Orn (Π S T ) u ∋ Π (T + : (s : S) → Orn (T s) u) Orn (Σ S T ) u ∋ Σ (T + : (s : S) → Orn (T s) u) -Delete S: | delete (s : S) (T + : Orn (T s) u) (O : Orn D u) orn : IDesc I insert S D + orn → Σ S λs. D + s orn var (inv i) orn → var i 1 orn → 1 Π T + orn → Π S λs. T + s orn Σ T + orn → Σ S λs. T + s orn delete s T + orn → T + orn DEFINITION Fig. 3: Universe of ornaments
datatype definition: we retrieve the set S from the index ornament D (which is equal to Σ S T for a Σ ornament, and to Π S T for a Π ornament). ▽

Remark (Inverse image 18

). The inverse of a function f is defined by the following inductive type

data [ f : A → B] -1 (b : B) : SET where f -1 (b = f a) ∋ inv (a : A)

DEFINITION

Equivalently, it can be defined with a Σ-type: ). An ornament is defined upon a base datatype -specified by a description D : func K -and a refined set of indices -specified by a function u :

( f : A → B) -1 (b : B) : SET f -1 b → (a : A) × f a = b ♦ 18 MODEL: Logic.Logic
I → K.
The ornament of D is an I-family of ornament codes for each D (u i), with i : I:

orn (D : func K) (u : I → K) : SET 1 orn D u → (i : I) → Orn (D (u i)) u (o : orn D u) orn : func I o orn → λi. o i orn

DEFINITION

In effect, ornamenting a description func consists merely in lifting the ornamentation of IDesc codes to a family indexed by I. ▽ 4.4 Remark (Overloaded notation). We overload the symbolorn to denote both the interpretation of an ornament code to a description code (Definition 4.1), and the interpretation of an ornament to a description (Definition 4.3). As for descriptions (Remark 3.4), the latter is merely of pointwise lifting of the former. ♦

Notation

As for inductive definitions, we adopt an informal notation to succinctly define ornaments.

The idea is to simply mirror our data definition, adding from which datatype the ornament builds upon. When specifying a constructor, we can then extend it with new information -using [x : S] -or delete an argument originally named x by providing a witness -using [x s]. We require the order of constructors to be preserved across ornamentation, as their name might change from the original to the ornamented version. This high-level notation enables us to succinctly specify ornaments. It provides an abstraction over the code of ornament, in the same manner that inductive definitions let us abstract over the code of description (Section 3.3). From the definition of an ornamented type T , we conventionally call T -Orn its ornament code. A formal description of the translation is beyond the scope of this article. Nonetheless, a few examples are enough to illustrate our notation and shall help us build some intuition for ornaments.

In an effort to reduce the syntactic noise, our notation for ornaments does not specify the forgetful function relating the indices of the ornamented type to its base type. For the examples given in this article, these functions can be inferred from the context. If in doubt, the reader should consult the corresponding definitions in the Agda model. In an actual implementation, the user would have to provide this information.

-Orn A → λ * . insert 'just 'nothing 'just → delete 'true (insert A λ -. 1) 'nothing → delete 'false 1
We leave it to the reader to verify that the interpretation of this ornament (byorn ) followed by the interpretation of the resulting description (by -) yields the signature functor of the option type X → 1 + A:

Maybe-Orn A orn X ∼ = 1 + A △ 4.6 Remark (Notation).
To reduce the notational burden, we overload the interpretation of ornamentsorn to denote both the description and the interpretation of that description. For instance, we write the above isomorphism as follows:

Maybe-Orn A orn X ∼ = 1 + A ♦ 4.7
Example (Ornamenting natural numbers to lists 21 ). We obtain lists from natural numbers with the following ornament:

data List [A : SET] from Nat where List A ∋ nil | cons [a : A](as : List A) List-Orn (A : SET) : orn Nat-func id List-Orn A → λ * . insert 'nil 'cons 'nil → delete '0 1 'cons → delete 'suc (insert A λ -. var (inv * ))
Unfolding the interpretations, we check that we obtain the signature functor of lists ). We obtain finite sets by inserting a number n ′ : Nat, constraining the index n to suc n ′ , and -in the recursive caseindexing at n ′ :

X → 1 + A × X: List-Orn A orn X ∼ = 1 + A × X △ 20 MODEL: Orn.Ornament.
data Fin (n : Nat) from Nat where

Fin n ∋ f0 [n ′ : Nat][q : n = suc n ′ ] | fsuc [n ′ : Nat][q : n = suc n ′ ](k : Fin n ′ )
Fin-Orn : orn Nat-func (λn. * )

Fin-Orn → λn. insert 'f0 'fsuc              'f0 → delete '0 (insert Nat λn ′ . insert (n = suc n ′ ) λ -. 1) 'fsuc → delete 'suc (insert Nat λn ′ . insert (n = suc n ′ ) λ -. var (inv n ′ ))             
Again, we leave it as an exercise to unfold the interpretations of this ornament and verify that it is indeed describing the signature of finite sets. △ 4.9 Example (Identity ornament23 ). In Section 2, we have introduced the identity ornament idO as the (trivial) ornament that merely duplicates the definition of its base type. This construction is a straightforward generic program over description codes:

idO (D : IDesc I) : Orn D id idO (var i) → var (inv i) idO 1 → 1 idO (Π S T ) → Π λs. idO (T s) idO (Σ S T ) → Σ λs. idO (T s)
which lifts then pointwise to ornaments: idO : (D : func I) → orn D id △ In Section 3.3, we had to adapt the original presentation of ornaments to our universe. In the process, we have discovered a new ornamental operation, namely the "deletion ornament". In Section 4.2, we explore some of the possibilities offered by having such a code in our system. However, we shall also verify that the ornamental constructions presented in the original framework still apply: this shall be the topic of Section 4.3where we recast the ornamental algebra in our setting -and Section 4.4 -where we recast the algebraic ornament construction. Finally, we revisit the algebraic ornament by the ornamental algebra in Section 4.5, making crucial use of the deletion ornament and of the optimisations discussed in the following section. In Example 3.8, we have seen an example of Brady's forcing and detagging optimisations, respectively on finite sets and vectors. We have explained how, thanks to our definition of descriptions as functions, we could (manually) craft datatypes in this form. Instead of a presentation based on constraints, we gave an equivalent but less redundant definition.

Seen as a datatype transformation, this operation is (obviously) structure-preserving. In fact, these transformations are an instance of ornamentation. The key ingredient is the delete code that lets us delete parts of a definition, using a witness extracted from the index. We can therefore craft our own Brady-optimised datatypes by ornamentation and benefit from this optimisation as early as at type checking.

To illustrate this approach, we give an example of detagging (Example 4.10) and forcing (Example 4.11). To focus solely on the Brady optimisations, we define these ornaments on the naive indexed family we wish to optimise. In practice, we would compose (Dagand & McBride, 2013a) the ornament of natural numbers (Example 1.4 (p.3) for vectors, and Example 4.8 for finite sets) with these optimisations. The composition would directly give the optimised version of, respectively, vectors and finite sets, thus avoiding an unnecessary duplication of isomorphic datatypes.

Example (Detagging, by ornamentation 24

). The definition of vectors in Example 3.7 mirrors Agda's convention of constraining indices with equality. Our definition of ornaments lets us define a version of Vec that does not store its indices. Indeed, we can describe Vec by an ornament that matches the index n to determine which constructor to offer:

data Vec' [A : SET](n : Nat) from Vec A n where Vec' A 0 ∋ nil Vec' A (suc n) ∋ cons [n ′ n](a : A)(vs : Vec' A n) Vec'-Orn (A : SET) : orn Vec-func id Vec'-Orn A 0 → insert {'nil} λ -. delete 'nil (delete refl 1) Vec'-Orn A (suc n) → insert {'cons} λ -. delete 'cons (delete n (delete refl (Σ λ -. var (inv n))))
Such a definition was unavailable in the original presentation of ornaments (McBride, 2013). We have internalised detagging: the constructors of the datatype are determined by the index. △ 4.11 Example (Forcing, by ornamentation25 ). The definition of finite sets given in Example 3.7 is also subject to an optimisation: by matching the index, we can avoid the duplication of n by deleting n ′ with the matched predecessor and trivialising the proofs. Hence, Fin can be further ornamented to the optimised Fin', which makes crucial use of

data Fin' (n : Nat) from Fin n where Fin' 0 ∋ [b : 0] Fin' (suc n) ∋ f0 [n ′ n] | fsuc [n ′ n](k : Fin' n ′ ) Fin'-Orn : orn Fin-func id Fin'-Orn 0 → insert 0 0-elim Fin'-Orn (suc n) → Σ 'f0 → delete n (delete refl 1) 'fsuc → delete n (delete refl (var (inv n)))
Note that when n is 0, there is in fact no constructor: we insert the empty set 0 to account for the absence of constructor at this index.

Again, this definition was previously unavailable to us. We have internalised forcing: the content of the constructors -here n ′ -are retrieved from the index, instead of being needlessly duplicated. △ 4.12 Remark (Non-generic transformations). The above transformations are ad-hoc: we have to manually give the ornament that performs the detagging and/or forcing. Because of the higher-order nature of our universe of descriptions, we cannot analyse the link between the indices, and the constructor choice and the constructor's contents. To achieve this from within type theory, we would need a first-order language for describing (a sufficiently expressive fragment of) the function space I → IDesc I. This is left to future work. ♦

Ornamental algebra

Every ornament induces an ornamental algebra (McBride, 2013): an algebra that forgets the extra information introduced by the extensions, mapping the ornamented datatype back to its original form.

4.13 Definition (Cartesian morphism 26 ). For an ornament O:Orn D u, there is a functionactually, a natural transformation (Dagand & McBride, 2013a) -projecting the ornamented functor down to the non-ornamented one (Fig. 4). This function then lifts pointwise to ornaments:

forgetNT : (o : orn D u) → o orn (X • u) i → D X (u i)
Orn D u) (xs : O orn (X • u)) : D X forgetNT (insert S D + ) (s, xs) → forgetNT (D + s) xs forgetNT (var (inv i)) xs → xs forgetNT 1 * → * forgetNT (Π T + ) f → λs. forgetNT (T + s) ( f s) forgetNT (Σ T + ) (s,
forgetAlg (o : orn D u) : o orn (µ D • u) i → µ D (u i) forgetAlg o → in •(forgetNT o) DEFINITION ▽ 4.
15 Definition (Forgetful map 27 ). In turn, this algebra induces a forgetful map from the ornamented type to its original form:

forget (o : orn D u) : µ o orn i → µ D (u i) forget o → forgetAlg o DEFINITION where (α : ∀ i. D X i → X i) : ∀ i. µ D i → X i
forget Fin-Orn (k : Fin n) : Nat forget Fin-Orn f0 → 0 forget Fin-Orn (fsuc k) → suc (forget Fin-Orn k) △ 4.
19 Example (From optimised finite sets to naïve finite sets 30 ). When an ornament relies on a delete operation, the forgetful map has the -perhaps counter-intuitive -task to reintroduce the deleted information into the base datatype. To do so, it simply uses the information obtained from the index to fill-in the deleted arguments. For example, the forgetful map obtained from Fin'-Orn corresponds to the following function:

forget Fin'-Orn (n : Nat) (k : Fin' n) : Fin n forget Fin'-Orn (suc n) f0 → f0 n refl forget Fin'-Orn (suc n) (fsuc k) → fsuc n refl (forget Fin'-Orn n k)
where, to be explicit about the origin of the recovered data, we pass the index n as an explicit argument. △

Algebraic ornaments

An important class of datatypes is constructed by algebraic ornamentation of a datatype. An algebraic ornament 31 indexes an inductive type by the result of a catamorphism over its elements. From the code D : func K and an algebra α : ∀ k. D X k → X k, we define the algebraic ornament, denoted D α , as the signature indexed by (k : K) × X k that satisfies the following coherence property:

For all k : K and x : µ D k, we have:

µ D α orn (k, x) ∼ = (t : µ D k) × α t = x (4.

27

Seen as a refinement type, this states that µ D α orn (k, x) is an inductive definition equivalent to the refinement type32 {t ∈ µ D k | α t = x}. A categorical presentation is given by [START_REF] Atkey | Refining inductive types[END_REF], who explore the connection between refinement types and inductive families.

The type-theoretic construction of D α was originally given by McBride (2013). We shall not reiterate it here, the implementation being essentially the same.The idea is to defineby ornamentation of D -a description whose fixpoint will satisfy the above coherence property.

4.21 Remark (Computational interpretation). Constructively, the coherence property (4.20) gives us two (mutually inverse) functions, coherentOrn and make D α .

The direction µ D α orn (k, x) → (t : µ D k) × α t = x relies on the generic forgetful map forget D α to compute the first component of the pair and gives us the following theorem33 :

coherentOrn : (t + : µ D α orn (k, x)) → α (forget D α t + ) = x

DEFINITION

This corresponds to the Recomputation theorem of McBride (2013). We shall not reprove it here, the construction being similar.

In the other direction, the isomorphism (4.20) gives us a function of type

(t : µ D k) × α t = x → µ D α orn (k, x)
which, after simplifying the equation, gives a function that lifts a datatype to its algebraic version 34 , at the index computed by the predicate:

make (D : func I) (α:∀ i. D X i → X i) : (t : µ D k) → µ D α orn (k, α t)

DEFINITION

This corresponds to the remember function of McBride (2013). Again, we will assume this construction here. ♦ 4.22 Example (Algebraic ornament: vectors). Ornamenting natural numbers to lists, we obtain an ornamental algebra: the algebra computing the length of a list. We can therefore build the algebraic ornament of lists by the length algebra 35 . This corresponds exactly to the datatype of vectors (Example 3.7): the resulting signatures are isomorphic, and both rely on constraints to enforce the indexing discipline.

Dagand and McBride

Note that this operation generalises to all ornaments: any ornament induces an ornamental algebra. Therefore, we can always build the algebraic ornament by the ornamental algebra. We shall study this operation in more details in Section 4.5.

m ≤ n ∼ = (k : Nat) × m + k = n
Put explicitly, the datatype computed by the algebraic ornament corresponds to

data [m : Nat] ≤ (n : Nat) : SET where m ≤ (n = m) ∋ 0 m ≤ (n = suc n ′ ) ∋ suc (k : m ≤ n ′ )
('const, n) → n evalAlg ('add, (m, n)) → m + n
Using the algebra evalAlg, we construct the algebraic ornament of Expr and obtain expressions indexed by their semantics:

data Expr evalAlg (k : Nat) : SET where Expr evalAlg (k = n) ∋ const (n : Nat) Expr evalAlg (k = m + n) ∋ add (m n : Nat)(d : Expr evalAlg m)(e : Expr evalAlg n)
We can now enforce the preservation of semantics by typing. For example, let us optimise away all additions of the form "0 + e": optimise-0+ (e : Expr evalAlg n) :

Expr evalAlg n optimise-0+ (const n) → const n optimise-0+ (add 0 n d e) → optimise

29

Because the type checker accepts our definition, we have that, by construction, this operation preserves the semantics. We can then prune the semantics from the types using the forgetful map and retrieve the transformation on raw syntax trees. The make function (Remark 4.21) lets us lift raw syntax trees to semantically-indexed ones, while the coherentOrn theorem (Remark 4.21) certifies that the pruned tree satisfies the invariant we enforced by indexing. △

Reornaments

In this article, we are particularly interested in a sub-class of algebraic ornaments. In Definition 4. Reornaments are thus straightforwardly obtained through a two steps process: first, compute the ornamental algebra and, second, construct the algebraic ornament by this algebra. However, such a simplistic construction introduces a lot of spurious equality constraints and duplication of information. For instance, using this naive definition of reornaments, a vector indexed by n is constructed as any list as long as it is of length n.

(i : I) × µ E (u i) → I) ⌈insert S D + ⌉ xs → Σ λs. ⌈D + s⌉ xs ⌈var (inv i)⌉ xs → var (inv (i, xs)) ⌈1⌉ * → 1 ⌈Π T + ⌉ f → Π λs. ⌈T + s⌉ ( f s) ⌈Σ T + ⌉ (s, xs) → delete s (⌈T + s⌉ xs) ⌈delete s T + ⌉ (s ′ , xs) → insert (s = s ′ ) λ -. ⌈T + ⌉ xs DEFINITION Fig. 5: Reornament
We can adopt a more fine-grained approach yielding an isomorphic but better structured datatype. In our setting, where we can compute over the index, a finer construction of the reornament of List-Orn is as follows:

• We retrieve the index, hence obtaining a number n : Nat;

• By inspecting the ornament List-Orn, we obtain the exact relationship between the index n and its ornament describing lists • If n = 0, we are in the first branch of the Σ code, and the ornamentation of n is necessarily the empty list. The corresponding reornament can therefore delete the choice of constructor (since it is entirely determined by the index), set it to '0, and terminate immediately:

⌈List-Orn A * ⌉ ('0, * ) delete '0 1

• If n = suc n ′ , we are in the second branch of the Σ code, and the ornament of suc n ′ is a necessarily non-empty list. Again, the corresponding reornament deletes the choice of constructor, by deducing from the index that it must be 'cons. Since the list ornament extends natural numbers with an argument of type A (through the insert code), we must preserve this information in the reornament (through a Σ code). Finally, we index the recursive argument of the reornamented datatype by n ′ :

⌈List-Orn A * ⌉ 'suc, n ′ delete 'suc (Σ λa. var (inv * , n ′ ))
Altogether, we have ornamented lists by their length: when the index is 0, the ornamented list is empty; when the index is suc n ′ , the ornamented list is non-empty and takes an argument indexed by n ′ . We have effectively described the datatype of vectors. △ Functional Ornaments 31 a var code, the reornament also duplicates the underlying structure by pairing the index of the ornament (provided by the index i) with the recursive argument of the base datatype (provided by the argument xs). On an insert code, the reornament preserves the extrainformation introduced by the ornament since it is absent from the index. However, on a Σ code, the ornament is merely duplicating information already provided by xs: in this case, we delete the argument, filling in the gap with the data provided by the index xs. On a delete code, we make sure -through an equality constraint -that the index xs is in sync with the data deleted by the ornament. This definition over codes then lifts pointwise to ornaments: ). Every ornament induces a reornament. A reornament is itself an ornament: it therefore induces yet another reornament. We are naturally led to wonder if this process ever stops, and if so when. For example, the ornament of natural numbers into lists reornaments to vectors. Reornamenting vectors, we obtain an inductive predicate representing the length function Length : Nat → List A → SET. Reornamenting Length leads to an object with no computational content: all its information has been erased and is provided by the indices.

⌈(o : orn D u)⌉ : orn o orn (π 0 : (i : I) × µ D (u i) → I) ⌈o⌉ → λ(i,
The same pattern arises in general: every chain of reornaments is bound to end with a computationally trivial object. We deduce this from our massaged definition of reornaments (Definition 4.29). To illustrate our reasoning, we simultaneously iterate the reornamentation of the following (artificial) ornament indexed by n : Nat We proceed by case analysis on the ornament. On a 1, Π, and var code, the reornamentation proceeds purely structurally, merely duplicating the ornament's code and introducing no information (Definition 4.29, first 3 cases). The reornamentation deletes Σ codes, using the indexing information (Definition 4.29, fourth case). On a delete code, the reornament inserts an equality constraint (Definition 4.29, sixth case), which contains no information per se: it is only enforcing the indexing discipline. Only on an insert code does the reornament introduce new information through a Σ code (Definition 4.29, fifth case). On our example, the first reornament is defined by Functional Ornaments

o + : orn ( o orn : func Nat) π 0 o + → ⌈o⌉ and unfolds to o + λ(n, in (a, f )). delete a (ΣC λc. Π λb. insert (true = π 0 ( f b)) λ -. var (inv (suc n, π 1 ( f b))))

33

In the subsequent iteration, these Σ codes in the reornament are in turn deleted by the re-reornament. On our example, the second reornamentation is defined by

o ++ : orn ( o + orn : Nat × µ D * ) π 0 o ++ → ⌈o + ⌉ and unfolds to o ++ λ((n, in (a, f )), in (a ′ , (c, f + ))). insert (a ′ = a) λ -. delete c (Π λb. Σ λq. var (inv ((suc n, π 1 ( f b)), f + b))
where the Σ code duplicates the (computationally trivial) equation on x, i.e. true = x.

In the third iteration, there is nothing left in the code but equations and structural scaffoldings (in the form of var, 1, and Π codes): the resulting datatype is computationally trivial and is entirely determined by its indices. On our example, the third reornamentation is defined by

o +++ : orn ( o ++ orn : func (n : Nat) × µ D * × µ o orn n) π 0 o +++ → ⌈o ++ ⌉ and unfolds to o +++ λ(((n, in (a, f )), in (a, (c, f + ))), in (c ′ , f ++ )). Σ λq 1 . insert (c ′ = c) λq 2 . Π λb. delete refl (var (inv (((suc n, π 1 ( f b)), f + b), π 1 ( f ++ b))))
where the Σ code duplicates the (computationally trivial) equation on a, i.e. a ′ = a. Formally, we have that any two inhabitants of a triple reornament are provably equal:

Let o : orn D u be an ornament. Let 1. i : I 2. ds : µ D (u i) 3. os : µ o orn i 4. os + : µ ⌈o⌉ orn (i, ds) be some indices. For any pair 1. xs : µ ⌈⌈⌈o⌉⌉⌉ orn (((i, ds), os), os + ) 2. ys : µ ⌈⌈⌈o⌉⌉⌉ orn (((i, ds), os), os + ) We have:

xs ∼ = ys

META-THEOREM

♦

In this section, we have adapted ornaments to our universe of datatypes. In doing so, we have introduced deletion ornaments, which rely on indexing to remove duplicated information from the datatypes. We shall see in Section 6 how this more careful definition can be turned to our advantage when we transport functions across ornaments. Ornaments provide us with a calculus of data-structures: from a given inductive family, we can ornament it to as many similarly-structured datatypes. The universe of ornaments is essentially an intensional characterisation of such structure-preserving transformation of datatype. Functional ornaments build upon ornaments (but not exclusively, as discussed in Remark 5.2), relying on them to capture the structural ties between the types of two functions, a base function and its lifting.

In that sense, the functional ornaments presented in this article are a generalisation of ornaments to function types. To describe them, we first need to be able to, intensionally and in type theory, manipulate function types. We thus define a universe of function types (Section 5.1). With it, we will be able to write generic programs over the class of functions captured by this universe. We define a functional ornament as a decoration over this universe (Section 5.2). The liftings implementing the functional ornament are related to the base function by a coherence property. To minimise the theorem-proving burden induced by coherence proofs, we expand our system with patches (Section 5.3): a patch is the type of the functions that satisfy the coherence property by construction. Finally, we show how we can project the lifting and its coherence certificate out of a patch (Section 5.4).

A universe of function types

5.1 Definition (Universe of types 44 ). For clarity of exposition, we restrict our language of types to the bare minimum: a type can either be an exponential whose domain is an inductive type, or a product whose first component is an inductive type, or the unit typeused as a termination marker:

data Type : SET 1 where Type ∋ µ{(D : func K) • (k : K) }→ (T : Type) | µ{(D : func K) • (k : K) }× (T : Type) | 1

DEFINITION

This universe codes the function space from some (maybe none) inductive types to some (maybe none) inductive types. Concretely, the codes are interpreted as follows: ). The constructions we develop next could be adapted to a more powerful universe -such as one supporting higher-order functions, non-inductive parameters, or including dependent quantifiers. However, this would needlessly complicate our exposition.

(T : Type) Type : SET µ{D • k }→ T Type → µ D k → T Type µ{D • k }× T Type → µ D k × T Type 1 Type → 1
For instance, the treatment of non-inductive parameters would lead to further, but orthogonal, extensions of the functional ornaments; namely, inserting or deleting these quantifiers during functional ornamentation. To support higher-order functions, we would have to distinguish the variance of ornamentations, a technicality that we can simply overlook in a first-order system. ♦ 5.3 Example (Coding -< -45 ). Written in the universe of function types, the type of the comparison function is

type< : Type type< → µ{Nat-func • * }→ µ{Nat-func • * }→ µ{Bool-func • * }× 1
The implementation of -<is essentially the same as earlier, excepted that it ought to return a pair of a Boolean and the inhabitant of the unit type. To reduce the syntactic noise introduced by this trivial multiplication by the unit, we assume that the type isomorphisms A × 1 ∼ = 1 × A ∼ = A are definitionally true: we spare ourselves from writing pairs with unit, and projections out of such pairs. Again, we refer our reader to the companion Agda code for the non-simplified terms.

To be explicit about the recursion pattern of this function, we make use of Epigram's by ( ⇐ ) gadget:

- < - : type< Type m < n ⇐ Nat-elim n m < 0 → false m < (suc n) ⇐ Nat-case m 0 < (suc n) → true (suc m) < (suc n) → m < n
That is, we first do induction on n and then, in the successor case, we proceed by case analysis over m. △ Again, up to a trivial multiplication by 1, the implementation of -+is left unchanged:

Example

-

+ -: type+ Type m + n ⇐ Nat-elim m 0 + n → n (suc m) + n → suc (m + n)
That is, it is defined by induction over m. △

Functional ornament

It is now straightforward to define functional ornaments: we traverse the function type and ornament the inductive types as we go. Note that it is always possible to leave an object non-ornamented: we ornament by the identity (Example 4.9), which simply copies the original description.

Definition (Universe of functional ornaments 47

). Following this intuition, we define functional ornaments by the following grammar:

data FunOrn (T : Type) : SET 1 where FunOrn (µ{D

• k }→ T ) ∋ ∀ u : I → K. µ + {(o : orn D u) • (i : u -1 k) }→ (T + : FunOrn T ) FunOrn (µ{D • k }× T ) ∋ ∀ u : I → K. µ + {(o : orn D u) • (i : u -1 k) }× (T + : FunOrn T ) FunOrn 1 ∋ 1 DEFINITION ▽ 5.
6 Definition (Lifting type47 ). We get the type of the liftings by interpreting the ornaments as we traverse the functional ornament:

(T + : FunOrn T ) FunOrn : SET µ + {o • inv i }→ T + FunOrn → µ o orn i → T + FunOrn µ + {o • inv i }× T + FunOrn → µ o orn i × T + FunOrn 1 FunOrn → 1 DEFINITION ▽
We want the ornamented function to be coherent with respect to the base function we started from: for a function f : µ D k → µ E l, the ornamented function f + of type

µ o D orn i µ o E orn j µ D (u i) µ E (v j) forget o D forget o E f f +
or, equivalently in type theory:

(x + : µ o D orn i) → f (forget o D x + ) = forget o E ( f + x + )
This captures our intuition that the lifted function f + behaves like the base function f , only that it also carries the extra-information introduced by the ornament o D over to the ornament o E . Coherence states that this extra-step does not interfere with its core operational behaviour, which is specified by f .

Definition (Coherence 48

). This definition of coherence generalises to any arity. We define it by induction over the code of functional ornaments:

Coherence (T + : FunOrn T ) ( f : T Type ) ( f + : T + FunOrn ) : SET Coherence (µ + {o • inv i }→ T + ) f f + → (x + : µ o orn i) → Coherence T + ( f (forget o x + )) ( f + x + ) Coherence (µ + {o • inv i }× T + ) (x, xs) (x + , xs + ) → forget o x + = x × Coherence T + xs xs + Coherence 1 * * → 1 DEFINITION ▽ 5.8
Example (Ornamenting type< to describe lookup49 ). In Section 2, we have identified the ornaments taking the type of -<to the type of lookup. We ornament Nat to List A (Example 4.7), and Bool to Maybe A (Example 4.5). From there, the functional ornament describing the type of the lookup function is as follows:

typeLookup : FunOrn type< typeLookup → µ + {idO Nat-func • inv * }→ µ + {List-Orn A • inv * }→ µ + {Maybe-Orn A • inv * }× 1
We leave it to the reader to verify that typeLookup FunOrn unfolds to the type of the lookup function, up to a multiplication by 1. Also, unfolding the coherence condition gives Coherence typeLookup (-< -) λ f + : typeLookup FunOrn .

(n : Nat)(xs

: List A) → isJust ( f + n xs) = n < length xs △ 5.9
Remark. This equation is not specifying the lookup function: it is only establishing a computational relation between -<and a candidate lifting f + , for which lookup is a valid choice. However, one could be interested in other functions satisfying this coherence property and they would be handled by our system just as well: the notion of functional ornament (Definition 5.5), and its coherence property (Definition 5.7) still apply. For example, assuming that A is a monoid, a function that sums the elements of List A from 0 to the index n, or returns nothing if the index is out of bound is coherent with -< -. ♦ 5.10 Example (Ornamenting type+ to describe -++ -50 ). The functional ornament of type+ relies solely on the ornamentation of Nat into List A:

type++ : FunOrn type+ type++ → µ + {List-Orn A • inv * }→ µ + {List-Orn A • inv * }→ µ + {List-Orn A • inv * }× 1
Again, we check that unfolding type++ FunOrn gives the type of -++while the coherence condition Coherence type++ (-+ -) correctly captures our requirement that appending lists preserves their lengths. As before, the list append function is not the only valid lifting: one could for example consider a function that reverses the first list and appends it to the second one. △

Patches

The coherence of the lifting f + : T + FunOrn of a base function f : T Type is therefore captured by the coherence predicate Coherence T + f . To implement a lifting that is coherent, we might ask the user to first implement the lifting f + and then prove its coherence. However, we find this process unsatisfactory: we fail to harness the power of dependent types when implementing f + , this weakness being then paid off by tedious proof obligations. To overcome this limitation, we define the notion of Patch as the type of all the functions that are coherent by construction.

5.11 Remark. We are looking for an isomorphism here: we will define patches in such a way that they are in bijection with the liftings satisfying a coherence property. Put otherwise, we want that: Functional Ornaments

Patch T T + f ∼ = ( f + : T + FunOrn ) × Coherence T + f f + ♦ 50 MODEL

39

In this article, we constructively exploit this bijection in the left-to-right direction: having implemented a patch f ++ of type Patch T T + f , we show how we can "apply" it, and extract a lifting together with its coherence proof.

5.12 Example (Patching -< -). Before giving the general construction of a Patch, let us first work through our running example. After having functionally ornamented -<with typeLookup, the lifting function f + and coherence property can be represented by the following commuting diagram:

Nat List A Maybe A Nat Nat Bool × × id -< - f + length isJust (5.13)
In type theory, this is written as

( f + : Nat × List A → Maybe A) × (m : Nat)(as : List A) → isJust ( f + m as) = m < length as
Applying intensional choice, this is isomorphic to

∼ = (m : Nat) × (n : Nat) × (as : List A) × length as = n → (ma : Maybe A) × isJust ma = m < n
Now, by the characterisation of reornaments (Equation 4.20), we have that:

(as : List A) × length as = n ∼ = Vec A n and

(ma : Maybe A) × isJust ma = b ∼ = IMaybe A b
Applying these isomorphisms, we obtain the following type, which we call the Patch of the functional ornament typeLookup:

∼ = (m : Nat) → (n : Nat) × (vs : Vec A n) → IMaybe A (m < n)
This last type is thus isomorphic to the pair of a lifting and its coherence proof. △

Intuitively, the Patch construction amounts to turning the vertical arrows of the commuting diagram (5.13) into the equivalent reornaments. In type-theoretic terms, it turns the pairs of datatypes and their algebraically defined constraints into the equivalent reornaments. The coherence property of reornaments (Equation 4.20) tells us that projecting the ornamented function down to its non-ornamented components gives back the base function. By turning the projection functions into inductive datatypes, we enforce the coherence property directly by the index: we introduce a fresh index for the arguments (in Example 5.12, introducing m and n) and index the return types by the result of the non-ornamented function (in Example 5.12, indexing IMaybe A by the result m < n). Patch (T : Type) For any function type T : Type, any functional ornament T + : FunOrn T of T , and any base function f : T Type , we have:

(T + : FunOrn T ) ( f : T Type ) : SET Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) f → (x : µ D (u i)) → µ ⌈o⌉ orn (i, x) → Patch T T + ( f x) Patch (µ{D • u i }× T ) (µ + {o • inv i }× T + ) (x, xs) → µ ⌈o⌉ orn (i, x) × Patch T T + xs Patch 1 1 * → 1 DEFINITION ▽ 5.
Patch T T + f ∼ = ( f + : T + FunOrn ) × Coherence T + f f + META-THEOREM
That is, our definition of the Patch type enforces that its inhabitants are exactly those liftings that are coherent by construction.

Proof. For clarity, we shall only write the proof for arity one. The generalisation to multiple input and output arities is straightforward but laboriously verbose. So, from a base function f : µ D k → µ E l, we start with its lifting and the associated coherence property:

( f + : µ o D orn i → µ o E orn j) × (ds + : µ o D orn i) → forget o E ( f + d + ) = f (forget o D ds + )
Applying intensional choice, we obtain the following isomorphic type:

∼ = (ds : µ D (u i)) × (ds + : µ o D orn i) × forget o D ds + = ds → (es + : µ o E orn j) × forget o E es + = f ds
Then, we can simply use the characterisation of reornaments (Equation 4.20) to turn every pair (x + :µ o X orn i) ×t = forget o X x + into the isomorphic inductive type µ ⌈o X ⌉ orn t:

∼ = (ds : µ D (u i)) × µ ⌈o D ⌉ orn ds → µ ⌈o E ⌉ orn ( f ds)
which corresponds to the Patch type of this functional ornament.

Remark (Computational interpretation)

. Constructively, we translate the left-to-right direction of this isomorphism into the pair of a patch function (Definition 5.22, which extracts the lifting) and a coherence proof (Definition 5.23, which establishes that such a lifting is coherent). ♦ 5.21 Remark (When to index?). While these precisely indexed functions relieve us from the burden of theorem proving, this approach is not always applicable. For instance, if we were to implement a length-preserving list reversal function, our patching machinery would ask us to implement vrev:

vrev (xs : Vec A n) : Vec A n vrev nil → nil vrev (cons a vs) → {(vrev vs) ++(cons a nil) : Vec A (1 + n)}
To complete this goal calls for some proving in order to match up the types: we must appeal to the equational theory of addition. Here, the term we put in the hole has type Vec A (n + 1) while the expected type is Vec A (1 + n). The commutativity of addition is beyond the grasp of most type checkers, which are often limited to deciding definitional identities.

In the case of vrev, unless the type checker works up to equational theories, as done in CoqMT [START_REF] Strub | Coq modulo theory[END_REF], the programmer is certainly better off using our machinery to generate the coherence condition (Section 5.2), implement the lifting, and write its coherence proof manually. While the patching machinery would still work, implementing a function realising the Patch specification would require some (cumbersome) rewritings of the types, thus littering the program with proofs.

This example gives a hint as to what can be seen as a "good" coherence property: because we want the type checker to do all the proving, the equations we rely on at the type level have to be definitionally true, either because our logic decides a rich definitional equality, or because we rely on operations that satisfy these identities by definition. ♦

Patching and coherence

At this stage, we can implement the ilookup function exactly as we did in Section 2.

From there, we now want to obtain the lookup function and its coherence certificate. More generally, having implemented a function satisfying the Patch type, we want to extract the lifting and its coherence proof. Perhaps not surprisingly, we obtain this construction by looking at the meta-theorem of the previous section (Theorem 5.19) through our constructive glasses: indeed, since the Patch type is isomorphic to the class of liftings satisfying the coherence property, we effectively get a function taking every Patch to a lifting (Definition 5.22) and its coherence proof (Definition 5.23). More precisely, we obtain the lifting by generalising the reornament-induced forget functions to functional ornaments while we obtain the coherence proof by generalising the reornament-induced coherentOrn theorem.

Definition (Patching 54

). We call patching the action of projecting the coherent lifting from a Patch function. Again, it is defined by induction over the functional ornament:

patch (T + : FunOrn T ) ( f : T Type ) ( f ++ : Patch T T + f ) : T + FunOrn patch (µ + {o • inv i }→ T + ) f f ++ → λx + . patch T + ( f (forget o x + )) ( f ++ (forget o x + ) (make ⌈o⌉ x + )) patch (µ + {o • inv i }× T + ) (x, xs) (x ++ , xs ++ ) → (forget

43

forget the ornament to compute f (forget o D x + ), and we can also make the reornament to compute f ++ (make ⌈o⌉ x + ). When an ornamented result is to be returned (i.e. with the code µ + {o • inv i }× ), we simply forget the reornamentation computed by the coherent lifting. ▽ 5.23 Definition (Coherence of a patch55 ). Extracting the coherence proof follows a similar pattern. We introduce arguments as we go, just as we did with patch. When we reach a result, we have to prove the coherence of the result returned by the patched function, which is a straightforward application of the coherentOrn theorem:

coherence (T + : FunOrn T ) ( f : T Type ) ( f ++ : Patch T T + f ) : Coherence T + f (patch T + f f ++ ) coherence (µ + {o • inv i }→ T + ) f f ++ → λx + . coherence T + ( f (forget o x + )) ( f ++ (forget o x + ) (make ⌈o⌉ x + )) coherence (µ + {o • inv i }× T + ) (x, xs) (x + , xs ++ ) → (coherentOrn x + , coherence T + xs xs ++ ) coherence 1 * * → * DEFINITION ▽ 5.
24 Example (Obtaining lookup and its coherence, for free56 ). This last step is a mere application of the patch and coherence functions. Hence, we define lookup as follows:

lookup : typeLookup FunOrn lookup → patch typeLookup (-< -) ilookup
And we get its coherence proof, here spelled in full (up to a multiplication by 1):

cohLookup (n : Nat) (xs : List A) : isJust (lookup n xs) = n < length xs cohLookup n xs → coherence typeLookup (-< -) ilookup n xs △ 5.
25 Remark (Code readability). The lookup function thus defined is rather daunting, especially for a potential user of that piece of code. However, we must bear in mind that lookup is in fact entirely specified by ilookup: there is no point in inspecting the definition of lookup. In a programming environment, we could imagine some syntactic sugar akin to our notation for ornaments. For example, we would state that lookup is a functional ornamentation of -< -. We would be lead to -transparently -implement ilookup in lieu of lookup. ♦

△

Looking back at the pedestrian construction of Section 2, we can measure the progress we have made. In the pedestrian approach, we had to (manually) index our datatypes (by defining Vec and IMaybe, and their projections back to, respectively, the list and option types), index the type signature of lookup (obtaining the type of ilookup), project lookup out of ilookup, and write its coherence proof (defining cohLookup from ilookup and the projection functions).

Functional ornaments let us focus on ornamenting the individual datatypes (Example 5.8). The rest is automatically generated for us: the coherence condition is computed by the generic Coherence type (Example 5.8), the indexed type of lookup is computed by the Patch type (Example 5.16), lookup is obtained by applying the patch (Example 5.24), and its coherence an instance of the generic coherence lemma (Example 5.24). This is not just convenient automation: a functional ornament establishes a strong connection between two functions. By pinning down this connection in this universe, we turn this knowledge into an effective object that can be manipulated and reasoned about within type theory.

We make use of this concreteness when we construct the Patch induced by a functional ornament: this is again a construction that is generic now, while we had to tediously (and perhaps painfully) construct it in Section 2. Similarly, we get patching and extraction of the coherence proof for free now, while we had to manually fiddle with several projection and injection functions.

We presented the Patch type as the type of the liftings coherent by construction. As we have seen, its construction and further projection down to a lifting is entirely automated, hence effortless. This is a significant step forward: we could either implement lookup and then prove it coherent, or we could go through the trouble of manually defining carefully indexed types and write a function correct by construction. Manually crafting these finely indexed types and functions takes up time and adds complexity to a code base. By automating these constructions, using finely indexed types is now just as economic (timewise and complexity-wise) as proving the coherence after the fact. From a programming perspective, the second approach is much more appealing. In a word, we have made an appealing technique extremely cheap! 5.27 Remark (No meta-theory). We must reiterate that none of the above constructions involve extending the type theory: building upon our universe of datatypes, ornaments

m < n ⇐ Nat-elim n m < 0 → false m < (suc n) ⇐ Nat-case m 0 < (suc n) → true (suc m) < (suc n) → m < n ilookup (m : Nat) (vs : Vec A n) : IMaybe A (m < n) ilookup m vs ⇐ Vector-elim vs ilookup m nil → nothing ilookup m (cons a vs) ⇐ Nat-case m ilookup 0 (cons a vs) → just a ilookup (suc m) (cons a vs) → ilookup m vs
Fig. 6: Implementations of -<and ilookup and functional ornaments are internalised as a few generic programs and inductive types. For systems such as Agda, Coq, or an ML with GADTs, we would need to extend the language -and therefore the meta-theory -to be able to reify inductive definitions, and provide an ornament mechanism. The fact that our constructions -such as the patching operations (Definition 5.22 and Definition 5.23), and the liftings (introduced in the next section, Definition 6.5, and Definition 6.17) type check in our model suggests that adding these objects at the meta-level is consistent with a pre-existing meta-theory. ♦ 5.28 Remark (Efficiency considerations). The patching framework relies crucially on the duality between a reornament and its ornament presentation subject to a proof. While patching (Definition 5.22), we cross this isomorphism in both directions. In effect, this involves a traversal of each of the input datatypes and a traversal of each of the output datatypes. However, operationally, these traversal are identities: the only purpose of these terms is at the logical level, for the type checker to fix the types. For example, the lookup function amounts to the following term:

lookup patch typeLookup (-< -) ilookup λm : Nat. λxs : List A. π 0 (forgetIMaybe (ilookup m (makeVec xs)))
In this definition, we rely on makeVec, which traverses the (input) list to return a vector indexed by the list's length. Operationally, this is an identity. We also rely on forgetIMaybe, which traverses the (output) IMaybe type to project it back to a non-indexed option type. Again, operationally, this is an identity.

In future work, we would like to transform our library of smart constructors into a proper domain-specific language (DSL). This way, implementing a coherent lifting would amount to working in a DSL for which an optimising compiler could compute away -by partial evaluation [START_REF] Brady | Scrapping your inefficient engine: using partial evaluation to improve domain-specific language implementation[END_REF]) -the computationally irrelevant operations. ♦ 6 Lazy Programmers, Smart Constructors

In our journey from -<to lookup, we had to implement the ilookup function. It is instructive to put -<and ilookup side-by-side (Fig. 6). First, both functions follow the same recursion pattern: induction over n/vs followed by case analysis over m. Second, the returned constructors are related through the Maybe ornament: knowing that we have returned true or false when implementing -< -, we can deduce which of just or nothing

Dagand and McBride

will be used in ilookup. Interestingly, the only unknown, hence the only necessary input from the user, is the a in the just case: this is precisely the information that has been introduced by the Maybe ornament.

In this section, we are going to leverage our knowledge of the definition of the base function -such as -< --to guide the implementation of the coherent lifting -such as ilookup: instead of re-implementing ilookup by duplicating most of the code of -< -, the user indicates what to transport and only provides the strictly-necessary inputs. We are primarily interested in transporting two forms of structure:

Recursion pattern: if the base function is a catamorphism α and the user provides us with a coherent algebra α ++ of α, we construct the coherent lifting α ++ of α ; Returned constructor: if the base function returns a constructor C and the user provides us with a coherent extension of C, we construct the coherent lifting of C.

We shall formalise what we understand by being a coherent algebra and a coherent extension below. The key idea is to identify the strictly-necessary inputs from the user, helped in that by the ornaments. It is then straightforward to build the lifted objects, automatically and generically.

Transporting recursion patterns

When transporting a function, we are very unlikely to change the recursion pattern of the base function. Indeed, the very reason why we can do this transformation is that the lifting uses exactly the same underlying structure to compute its results. Hence, most of the time, we could just ask the computer to use the recursion pattern induced by the base function: the only task left to the user will be to give an algebra.

Example (Lifting a catamorphism).

To understand how we transport recursion patterns, let us look again at the coherence property of liftings, but this time specialising to a function that is a catamorphism:

µ o D orn i µ o E orn i µ D (u i) µ E (u i) forget o D forget o E α β
By the fold-fusion theorem [START_REF] Bird | Algebra of programming[END_REF], it is sufficient to work on the algebras, where we have the following diagram:

o D orn (µ o E orn ) i µ o E orn i o D orn (µ E • u) i D (µ E) (u i) µ E (u i) o D orn → (forget o E ) forgetNT o D forget o E α β

47

We can therefore reduce the problem of describing the commuting square of catamorphisms (i.e. the Patch of α ) to the one consisting in working directly with their algebras. In effect, we are going to characterise the algebras α ++ whose catamorphism is coherent by construction (i.e. inhabits the Patch of α ). △ 6.2 Remark. We have established that if the square composed of the algebras commutes, then the square composed of their catamorphisms commutes. However, the converse does not hold: having that the square of catamorphisms commutes does not necessarily imply that the square of algebras commutes. ♦

Example (Lifting isSuc).

To illustrate our approach, let us work through a concrete example: we derive hd : List A → Maybe A from isSuc : Nat → Bool by transporting the algebra. For the sake of argument, we artificially define isSuc by a catamorphism:

isSuc (n : Nat) : Bool isSuc n → isSucAlg n where isSucAlg (xs : Nat-func (λ * . Bool) * ) : Bool isSucAlg ('0, * ) → false isSucAlg ('suc, xs) → true
Our objective is thus to define the algebra for hd, which has the following type

hdAlg : List-func A (λ * . Maybe A) * → Maybe A
such that its catamorphism is coherent. By the fold-fusion theorem, it is sufficient for hdAlg to satisfy the following condition:

(ms : List-func A (λ * . Maybe A) * ) → isJust (hdAlg ms) = isSucAlg (forgetNT (List-Orn A) ( List-func A → isJust ms))
Following the same methodology we applied to define the Patch type, we can massage the type of hdAlg and its coherence condition to obtain an isomorphic definition enforcing the coherence by indexing. In this case, we obtain the type

lift Alg hdAlg ∀ n. Vec-func A (λn ′ . IMaybe A (isSuc n ′ )) n → IMaybe A (isSuc n) △
This construction generalises to any functional ornament. First, we define the notion of coherent algebra (Definition 6.4) as those algebras that are coherent by construction. We then compute the coherent liftings of these algebras (Definition 6.5). ). We define the coherent algebras over an algebra α to be the inhabitants of the type

lift Alg (α : ∀ k : K. D (λ -. T Type ) k → T Type ) (o : orn D u) (T + : FunOrn T ) : SET lift Alg α o T + → ∀ (i,t) : (i : I) × µ D (u i). ⌈o⌉ orn (λ(i,t). Patch T T + ( α t)) (i,t) → Patch T T + ( α t) DEFINITION ▽ 6.
5 Definition (Lifting of coherent algebra 58 ). Constructively, we get that coherent algebras induce coherent liftings, by the catamorphism of the coherent algebra:

lift-fold (α : ∀ k : K. D (λ -. T Type ) k → T Type ) (α ++ : lift Alg α o T + ) : Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) α lift-fold α α ++ → λx. λx ++ . α ++ x ++ DEFINITION ▽
The treatment of induction is essentially the same, as hinted at by the fact that induction can be reduced to a catamorphism [START_REF] Hermida | Structural induction and coinduction in a fibrational setting[END_REF]. We first define the coherent inductive step and deduce an operation lifting induction principles: 6.6 Definition (Coherent inductive step 59 ). We define the coherent inductive step over an inductive step α to be the inhabitants of the type Functional Ornaments 49 6.7 Definition (Lifting of inductive step 60 ). As for algebras, a coherent inductive step α ++ induces a coherent lifting, by merely applying the induction:

lift IH (α : (k : K)(xs : D (µ D) k) → D (λ -. T Type ) xs → T Type ) (o : orn D u)(T + : FunOrn T ) : SET lift IH α o T + → ((i,t) : (i : I) × µ D (u i)) → (xs : ⌈o⌉ orn (µ ⌈o⌉ orn ) (i,t)) → ⌈o⌉ orn (λ(i,t). Patch T T + (induction α t)) xs → Patch T T + (
lift-ind (α : (k : K)(xs : D (µ D) k) → D (λ -. T Type ) xs → T Type ) (α ++ : lift IH α o T + ) : Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) (induction α) lift-ind α α ++ → λx. λx ++ . induction α ++ x ++ DEFINITION ▽ 6.
8 Definition (Lifting of case analysis 61 ). Lifting case analysis is trivial, since it is derivable from induction by stripping out the induction hypotheses (McBride et al., 2004):

lift-case (α : (k : K)(xs : D (µ D) k) → T Type ) (α ++ : lift IH (λxs -. α xs) o T + ) : Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) (induction (λxs -. α xs)) lift-case α α ++ → lift-ind (λxs -. α xs) (λxs -. α ++ xs) DEFINITION ▽
6.9 Example (Transporting the recursion pattern of isSuc 62 ). We can now apply our generic machinery to transport isSuc to hd: using a high-level notation, we write the command of Fig. 7(a) (p.55). This command instructs the system to generate the skeleton of the algebra, as shown in Fig. 7(b) (p.55). In the low-level type theory, this corresponds to the following term:

ihd (vs : Vec A n) : IMaybe A (isSuc n) ihd vs → lift-fold isSucAlg ihdAlg vs where ihdAlg (vs : Vec-func A (λn ′ . IMaybe A (isSuc n ′ )) n) : IMaybe A (isSuc n) ihdAlg ('nil, * ) → {?} ihdAlg ('cons, (a, xs)) → {?}
Note that we do not need to specify the arguments over which the catamorphism is lifted in Fig. 7(a): indeed, this information is provided by the base function. This is reflected by the elaborated code: the arguments of lift-fold are only the algebras. The resulting catamorphism is applied to the correct variables, by construction. △ . Formalising the elaboration process from the highlevel notation to the low-level type theory is beyond the scope of this article. The reader will convince herself that the high-level notation contains all the information necessary to reconstruct a low-level term. Indeed, when lifting a recursion pattern, the goal -a Patch type -provides all the information concerning the functional ornament being constructed, including the algebra that is being lifted. Similarly, when lifting a constructor, the goal -still a Patch type -carries the functional ornament as well as the constructor being lifted. We shall use the high-level notation to succinctly describe our transformations, with the understanding that it builds a low-level term that type checks. We come back the practicality of such a notation in Remark 6.22. ♦ 6.11 Example (Transporting the recursion pattern of -< -63 ). To implement ilookup, we use lift-ind to transport the induction over n:

ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs lift ⇐ lift-ind ilookup m m + 0 nil {?} ilookup m m + (suc n) (cons a vs) {?}
Followed by a lift-case to transport the case analysis over m:

ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs lift ⇐ lift-ind ilookup m m + 0 nil {?} ilookup m m + (suc n) (cons a vs) lift ⇐ lift-case ilookup 0 0 0 nil {?} ilookup (suc m) (suc m + ) 0 nil {?}
The interactive nature of this construction is crucial: the user needs only to specify a lifting -symbolised by the lift ⇐ command -together with the action to be carried out, while the computer does all the heavy lifting and generates the resulting patterns. △ 6.12 Example (Transporting the recursion pattern of -+ -64 ). In order to implement the concatenation of vectors, we can also benefit from our generic machinery. We simply have to instruct the machine that we want to lift the case analysis used in the definition of -+and the computer comes back to us with the following goals: Just as the recursive structure, the returned values frequently mirror the original definition: we are often in a situation where the base function returns a given constructor and we would like to return its ornamented counterpart. Informing the computer that we simply want to lift that constructor, it should fill in the parts that are already determined and ask only for the missing information, i.e. the data newly introduced by the ornament.

Recall that, when constructing an inhabitant of a Patch type, we are working on the reornaments of the lifting. When returning a constructor-headed value, we are simply building an inhabitant of a reornament (Definition 5.15, case µ + {o • inv i }× ). By definition of reornaments (Section 4.5), all the information provided by the non-ornamented datatype -the index -is optimally used: every opportunity for deletion has been taken. In particular, none of the data provided by index -the non-ornamented data -needs to be duplicated within the reornamented datatype: only the extensions introduced by the ornament need to be provided.

This suggests a decomposition of the inhabitants of reornaments in two components:

• Giving the extension of the ornament, i.e. all the extra information introduced by the ornament; • Giving the recursive arguments -dictated by its structure -of the reornamented datatype.

6.13 Example (Inhabiting the reornament of List-Orn). Let us illustrate this decomposition on the reornament of List-Orn. The reornament of List-Orn is structured as follows:

• We retrieve the index, hence obtaining a number n : Nat;

• By inspecting the ornament List-Orn, we obtain the exact information by which n is extended into a list: if n = 0, no supplementary information is needed; if n = suc n ′ , we need to extend it with an a : A. We call this the extension -denoted Extensionof List-Orn at n:

Extension (List-Orn A * ) ('0, * ) 1 Extension (List-Orn A * ) 'suc, n ′ (a : A) × 1
• By inspecting the ornament List-Orn again, and provided an extension of the index n, we obtain the recursive structure of the reornament at that index by extracting the refined indexing discipline: if n = 0, no argument is expected; if n = suc n ′ , we expect the tail to be a vector of size n ′ . We call this the (recursive) structure -denoted Structure -of List-Orn at n:

Structure (List-Orn A * ) ('0, * ) * 1 Structure (List-Orn A * ) 'suc, n ′ (a, * ) µ ⌈List-Orn A⌉ orn * , n ′
Provided an extension -an inhabitant e of Extension (List-Orn A * ) n -and its recursive arguments -an inhabitant of Structure (List-Orn A * ) n e, we have all the necessary data to inhabit of reornament of List-Orn (i.e., to inhabit a vector indexed by n). △ ZU064-05-FPR paper 13 December 2013 17:37 52

Dagand and McBride

This decomposition generalises to any reornament. We define the extension of an ornament (Definition 6.14), and the structure of its reornament (Definition 6.15). Given an extension and its structure, we then show how to inhabit a reornament (Definition 6.16). In what follows, we take E : func I to be a description and o : orn E u to be an ornament of E.

6.14 Definition (Reornament extension65 ). The extension of an ornament is given by its insert codes. Therefore, the Extension function merely collects these insertions (the insert case). It also makes sure that the indexing respects the previously deleted data through equations (the delete case). On a Σ case, no data is required: the information is already available from the index. Otherwise, it proceeds purely structurally (the var, 1, and Π cases).

Extension (var (inv i)) xs → 1 Extension 1 * → 1 Extension (Π T + ) f → (s : S) → Extension (T + s) ( f s) Extension (Σ T + )
(s, xs) → Extension (T + s) xs -Deleted data must be consistent with the index:

Extension (delete s T + ) (s ′ , xs) → (q : s = s ′ ) × Extension T + xs

DEFINITION

Note that while we copy the Π codes as a Π-type, we are not duplicating information: the codomain of the Π-type contains only new information, or is isomorphic to 1 (in which case, the whole Π-type is itself isomorphic to 1). ▽

META-THEOREM

In practice, we are interested in the left-to-right direction of the isomorphism, which allows us to inhabit a reornament by focusing on the extension introduced by the ornament and its recursive arguments. Constructively, this translates into the mkReorn function below.

6.16 Definition (Inhabitation of reornaments66 ). For a given ornament O : Orn D u and some index xs : D (µ E), we can therefore combine an extension of O at xs with its recursive arguments to inhabit the reornament of O. To do so, we proceed by case analysis over the ornament O: we find that the data required by the reornament is either provided by the extension (case insert), or the structure (case var). The other cases contain no data ). As for ilookup, we want to lift the constructors true and false to the Maybe ornament. In a high-level notation, this would be represented as follows:

ihd (vs : Vec A n) : IMaybe A (isSuc n) ihd lift ⇐ lift-fold where ihdAlg (vs : Vec-func (λn ′ . IMaybe A (isSuc n ′ )) n) : IMaybe A (isSuc n) ihdAlg 'nil { lift → } ihdAlg ('cons a xs) { lift → } (
ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs lift ⇐ lift-ind ilookup m m + 0 nil lift → nothing * [ * ] ilookup m m + (suc n) (cons a vs) lift ⇐ lift-case ilookup 0 0 (suc n) (cons a vs) lift → just {a : A} [ * ] ilookup (suc m) (suc m + ) (suc n) (cons a vs) {?}
As before, in an interactive setting, the user would instruct the machine to execute the command lift → and the computer would come back with the skeleton of the expected inputs. Finishing the implementation of ilookup is now a baby step away for the programmer:

ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs lift ⇐ lift-ind ilookup m m + 0 nil lift → nothing * [ * ] ilookup m m + (suc n) (cons a vs) lift ⇐ lift-case ilookup 0 0 (suc n) (cons a vs) lift → just a[ * ] ilookup (suc m) (suc m + ) (suc n) (cons a vs) → ilookup m m + n vs
This last step is out of reach of our framework: the recursive call is justified by the first induction over the vector vs, which gives us access to an higher-order induction hypothesis (taking natural numbers to the IMaybe type). We have to fully apply this induction hypothesis to m and im to perform the recursive call, an operation for which can offer no support. △ 6.20 Remark (Lifting vs. manual construction). Had we ignored the structural ties between -<and lookup, we would have constructed ilookup by duplicating its underlying structure:

ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs ⇐ Vector-elim vs ilookup m m + 0 nil → nothing ilookup m m + (suc n) (cons a vs) ⇐ Nat-case m + ilookup 0 0 (suc n) (cons a vs) → just a ilookup (suc m) (suc m + ) (suc n) (cons a vs) → ilookup m m + n vs
That is, we would have duplicated the induction over the second argument (. . . ⇐ Vec-elim vs), and the induction over the first argument (. . . ⇐ Nat-elim m). We would also have duplicated the returned constructor (. . . → nothing and . . . → just a).

Ignoring the structural ties has two consequences. First, this provides less opportunities for the system to guide the implementation of ilookup: the search space is less constrained.

57

Second, having lost the connection between -<and ilookup, a modification of the former will not impact the latter. In the course of a development, the two implementations might diverge in incompatible ways. ♦ 6.21 Example (Transporting the constructors of -+ -70 ). We can also benefit from the automatic lifting of constructors to fill out the cons case of vector append. We instruct the system that we want to lift the suc constructor, which results in the following goals: 22 Remark (About an interactive system). To convey our message to the reader, we have used an (informal) notation, extending the Epigram programming gadgets with liftingspecific gadgets. We have not given much information about their implementability, or even hinted at a formal specification. It would certainly be interesting to elaborate on such a language extension. However, as for the notation for ornaments (Section 4.1), this notation was meant to convey high-level intuitions to the reader, and to keep us from flooding these pages with lambda terms. In terms of implementation, elaborating this notation (or a less ambiguous version thereof) might reveal arduous. A more pragmatic alternative would be to implement a semi-decision procedure à la Agsy [START_REF] Lindblad | A tool for automated theorem proving in Agda[END_REF]) that would attempt to automatically lift a function. In this setting, the lifting constructors we have defined in this section serve as a precise language in which to express the lifting problem, and over which to compute its solution. They thus narrow the search-space and guide the decision procedure. 2013) on ornaments, originally introduced to organise datatypes according to their common structure. This gave rise to the notion of ornamental algebras -forgetting the extra information of an ornamented datatype -and algebraic ornaments -indexing a datatype according to an algebra. This, in turn, induced the notion of algebraic ornament by ornamental algebras, which is a key ingredient for our work. However, for simplicity of exposition, these ornaments had originally been defined on a less index-aware universe of datatypes. As a consequence, computation over indices was impossible and deletion of duplicated information was impossible. A corollary of this was that reornaments contained a lot of duplication, hence making the lifting of values from ornamented to reornamented datatypes extremely tedious.

Our presentation of algebraic ornament has been greatly improved by the categorical model developed by [START_REF] Atkey | Refining inductive types[END_REF]: the authors gave a conceptually clear treatment of algebraic ornament in a Lawvere fibration. At the technical level, the authors connected the definition of algebraic ornament with truth-preserving liftings, which are also used in the construction of induction principles, and op-reindexing, which models Σ-types in type theory. Whilst the authors did not explicitly address the issue of transporting functions across ornaments, much of the infrastructure was implicitly there: for instance, lifting of catamorphisms is a trivial specialisation of induction.

In their work on realizability and parametricity for Pure Type Systems, [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF] have shown how to build a logic from a programming language. In such a system, terms of type theory can be precisely segregated based on their computational and logical contribution. In particular, the idea that natural numbers realise lists of the corresponding length appears in this system under the guise of vectors, the reflection of the realizability predicate. The strength of the realizability interpretation is that it is naturally defined on functions: while McBride (2013) and [START_REF] Atkey | Refining inductive types[END_REF] only consider ornaments on datatypes, Bernardy and Lasson's work is the first, to our knowledge, to capture a general notion of functions realisingi.e. ornamenting -other functions.

Bernardy and Moulin has further shown that this technique can be internalised in a type theory with color [START_REF] Bernardy | Type-theory in color[END_REF], for which the logical system and the programming language are a single entity. In this setting, the realizability predicate is specialised to an (internalised) parametricity result. This parametricity result gives "theorems for free" [START_REF] Wadler | Theorems for free! Pages 347-359 of: Conference on functional programming languages and computer architecture[END_REF], relating functions operating on colored types (akin to our functional ornaments) to functions operating on color-erased types (akin to our base types). On inductive types, colors allow a user to specify restrictions of types (dually to the extension mechanism offered by ornaments), by filtering out some colors from a definition. This difference is mostly methodological. Our work is focused on creating more precise datatypes from less precise ones, and lifting functions from basic types to richer types: hence our focus on extensions. Being guided by erasure, Bernardy and Moulin focus on extracting functions on less precise types from the more informative ones: hence their focus on restrictions. In our setting, the erasure-based approach corresponds to the right-to-left direction of the Patch isomorphism (Theorem 5.19). The refinement mechanism offered by ornaments seems absent from the initial proposal of the calculus of colored constructions: this suggests a natural generalisation of the calculus with inductive families. Our base types Functional Ornaments 59 and functional ornaments are however limited to a first-order, simply-typed setting, whilst the calculus of colored constructions defines erasure for Π-types and Σ-types: it would be interesting to extend our universe of function types and functional ornaments in that direction (following Remark 5.2). Following the steps of Bernardy and Lasson, Ko and Gibbons (2011) adapted the realizability interpretation to McBride's universe of datatypes and explored the other direction of the Patch isomorphism (Theorem 5.19), using reornaments to generate coherence properties: they describe how one could take list append together with a proof that it is coherent with respect to addition and obtain the vector append function. Their approach would shift neatly to our index-aware setting, where the treatment of reornaments is streamlined by the availability of deletion.

However, we prefer to exploit the direction of the isomorphism which internalises coherence: we would rather use the full power of dependent types to avoid explicit proof. Hence, in our framework, we simultaneously induce list append and implicitly prove its coherence with addition just by defining vector append. Of course, which approach is appropriate depends on one's starting point. Moreover, our universe of function types takes a step beyond the related work by supporting the mechanised construction of liftings, leaving to the user the task of supplying a minimal patch. Our framework could easily be used to mechanise the realizability predicates of [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF], and [START_REF] Ko | Modularising inductive families[END_REF].

Conclusion

In this article, we have adapted McBride's ornaments to our universe of datatypes, a cosmetic evolution of an earlier presentation [START_REF] Chapman | The gentle art of levitation[END_REF] . This gave us the ability to compute over indices, hence introducing the deletion ornament. Deletion ornaments are a key ingredient for the internalisation of Brady's optimisation over inductive families. By applying these ideas, we obtained a simpler implementation of reornaments.

We then developed the notion of functional ornament as a generalisation of ornaments to functions: from a universe of function type, we define a functional ornament as the ornamentation of each of its inductive components. A function of the resulting type will be subject to a coherence property, akin to the ornamental forgetful map of ornaments. We have constructively presented this object by building a small universe of functional ornaments.

We have finally shown how to achieve code reuse by transporting functions along a functional ornament in such a way that the coherence property holds. Instead of asking the user to write cumbersome proofs, we defined a Patch type as the type of all the functions that satisfies the coherence property by construction. Hence, we make extensive use of the dependently-typed programming machinery: in this setting, the type checker, that is the computer, is working with us to construct a term, not waiting for us to produce a proof.

Having implemented a function correct by construction, one then gets, for free, the lifting and its coherence certificate. This is a straightforward application of the isomorphism between the Patch type and the set of coherent functions. These projection functions have been implemented in type theory by simple generic programming over the universe of functional ornaments. To further improve code reuse, we provide a few smart constructors to implement a Patch type: the idea is to use the structure of the base function to guide the implementation of the coherent lifting. Hence, if the base function uses a specific induction principle or returns a specific constructor, we make it possible for the user to specify that she wants to lift this structure one level up. This way, the function is not duplicated: only the new information, as determined by the ornament, is necessary.

To conclude, we believe that this is a first yet interesting step toward code reuse for dependently-typed programming systems. With ornaments, we were given the ability to organise datatypes by their structure. With functional ornaments, we are now able to organise functions by their structure-preserving computational behaviour. For a large class of functional ornaments, the original program and its lifting share a similar recursion pattern and returned value. To take advantage of this structural similarity, we have developed some appealing automation to assist their implementation, without any proving required, hence making this approach even more accessible. Future work Whilst we have deliberately chosen a simple universe of types, we plan to extend it in various directions. Supporting higher-order functions and adding type dependency (Π-types and Σ-types) is a necessary first step. Inspired by [START_REF] Bernardy | Realizability and parametricity in pure type systems[END_REF], we would like to add a parametric quantifier: in the implementation of ilookup, we would mark the index A of List A as parametric so that in the cons a case, the a could automatically be carried over.

The universe of functional ornaments could be extended as well, especially once the universe of function types has been extended with dependent quantifiers. For instance, we want to consider the introduction and deletion of quantifiers, as we are currently doing on datatypes. Whilst we have only looked at least fixpoints in this article, we also want to generalise our universe with greatest fixpoints and the lifting of co-inductive definitions.

Besides enriching the universe, its systematic exploration offers exciting prospects. For pedagogical reasons, this article is confined to a handful of ornaments (natural numbers to lists, Booleans to the option type, etc.) and focuses on two functional ornaments (the comparison and the addition). A quick comparison between natural numbers and lists reveals a few other opportunities, such as the --/drop, null/head, or pred/tl. Keeping with non-indexed data-structures, a whole zoo of ornaments is available for tree-like structures, depending on whether one stores the data at the leaves, nodes, or both. One could imagine writing the structural operations on the bare structure and to instantiate them for specific data-storage strategies by lifting. Finally, the indexed setting -where ornaments find their raison d'être -is the most promising. For example, we would like to exploit the fact that the simply-typed lambda-calculus (Example 3.10) is an ornament of the untyped one and lift its substitution operators from the one defined over the untyped calculus.

ZU064

  List A) ++ (ys : List A) : List A nil ++ ys → ys (cons a xs) ++ ys → cons a (xs ++ ys)or, from subtraction of natural numbers to dropping a prefix:(m : Nat) -(n : Nat) suc m) -(suc n) → mn ⇒ drop (xs : List A) (n : Nat) : List A drop nil n → nil drop xs 0 → xs drop (cons a xs) (suc n) → drop xs n

  Fig. 1: Implementation of -<and lookup

  where IMaybe A is the option type indexed by the truth value computed by isJust. It is defined as follows data IMaybe [A : SET](b : Bool) : SET where IMaybe A (b = true) ∋ just (a : A) IMaybe A (b = false) ∋ nothing and it comes with a forgetful map: forgetIMaybe (ima : IMaybe A b) : (ma : Maybe A) × isJust ma = b forgetIMaybe (just a) → (just a, refl) forgetIMaybe nothing → (nothing, refl)

Fig. 2 :

 2 Fig. 2: Universe of inductive families

  (Descriptions 3 ). We obtain the universe of descriptions func by simply pulling the I-index to the front. The interpretationextends pointwise to func:func (I : SET) : SET 1 func I → I → IDesc I (D : func I) (X : I → SET) : I → SET D X → λi. D i X TYPE THEORY

  (Ornament: from Booleans to the option type 20 ). We obtain the option type from the Booleans by inserting an extra a : A in the true case: data Maybe [A : SET] from Bool where Maybe A ∋ just [a : A] | nothing Maybe-Orn (A : SET) : orn Bool-func id Maybe

  △ 4.23 Example (Algebraic ornament: less-than-or-equal relation 36 ). For a given natural number m : Nat, the addition m + -: Nat → Nat is obtained by folding the algebra plusAlg (m : Nat) (xs : Nat-func Nat * ) : Nat plusAlg m ('0, * ) → m plusAlg m ('suc, n) → suc n By ornamenting Nat by this algebra, we obtain the relation m ≤ -: Nat → SET that is characterised by the isomorphism

△ 4 .

 4 24 Example (Algebraic ornament: indexing by semantics 37 ). A typical use-case of algebraic ornaments is the implementation of semantic-preserving operations (McBride, 2013). For example, let us consider arithmetic expressions, whose semantics is given by interpretation to Nat: data Expr : SET where Expr ∋ const (n : Nat) | add (d : Expr)(e : Expr) evalAlg (es : Expr-func Nat * ) : Nat evalAlg

  4.28 Example (Reornamenting vectors, efficiently). Let us consider the ornament List-Orn, taking natural numbers to lists. We gave its code in Example 4.7. Here, for simplicity, we shall work on the following variant List-Orn (A : SET) : orn Nat-func id List-Orn A → λ * . Σ '0 → 1 'suc → insert A λ -. var (inv * ) which does not update the constructor names, allowing us to focus on the essential steps. : Orn D u)⌉ (xs : D (µ E)) : Orn O orn (π 0 :

4. 29

 29 Definition (Reornament 38 ). A reornament (Fig.5) is thus defined over an ornament code O : Orn D u (for some description D : IDesc I) and an index belonging to the base datatype xs: D (µ D). On the 1 and Π codes, the reornament simply mirrors the underlying ornament, while peeling off the index: the structure of the three datatypes is identical. On 38 MODEL: Orn.Reornament

o

  : orn D (λn. * ) o → λn. Σ λa. insertC λc. Π λb. delete true (var (suc n)) which ornaments the description D : func 1 D → λ * . Σ A λa. Π B λb. Σ Bool λx. var * where A, B, and C are sets.

  of Function Types and their Ornaments

  Remark (Terminology). The name of "patch" comes from the idea that the Patch type Patch T T + f captures all those (coherent) functions that extends the base function f . In Section 5.4, we shall see how such a patch can be applied (Definition 5.22), i.e. we describe how a base function is patched by an inhabitant of a Patch type to build its coherent lifting. ♦ 5.15 Definition (Patch type 51 ). We define the Patch type generically by induction over the functional ornament. Upon an argument (i.e. a code µ + {o • inv i }→ ), we introduce a fresh index and the reornament of o. Upon a result (i.e. a code µ + {o • inv i }× ), we ask for a reornament of o indexed by the result of the base function.

  16 Example (Patch of typeLookup 52 ). The type of the coherent liftings of -<by typeLookup, as defined by the Patch of -<by typeLookup, unfolds to (m : Nat)(m + : µ ⌈idO Nat-func⌉ orn m) → (n : Nat)(vs : µ ⌈List A⌉ orn n) → µ ⌈Maybe A⌉ orn (m < n) × 1 △ 5.17 Remark. µ ⌈idO Nat-func⌉ orn m is isomorphic to 1: all the content of the datatype has been forced -the recursive structure of the datatype is entirely determined by its index -and detagged -the choice of constructors is entirely determined by its index, leaving no actual data in it. Being computationally uninteresting, we ignore this argument. On the other hand, ⌈List A⌉ and ⌈Maybe A⌉ are, respectively, the previously introduced vectors (Example 4.30) and indexed option (Example 4.31) types. ♦ 5.18 Example (Patch of type+ 53 ). Similarly, the Patch of -+by type+ unfolds to the type of the vector append function (m:Nat)(xs:µ ⌈List A⌉ orn m) → (n:Nat)(ys:µ ⌈List A⌉ orn n) → µ ⌈List A⌉ orn (m + n) × 1 where, again, the datatype µ ⌈List A⌉ orn corresponds exactly to vectors. △ MODEL: FunOrn.Patch MODEL: FunOrn.Patch.Examples.Lookup MODEL: FunOrn.Patch.Examples.Append Theorem. Following our Remark 5.11, we have that a Patch is isomorphic to the pair of a lifting and its coherence proof:

  60 MODEL: FunOrn.Lift.Induction 61 MODEL: FunOrn.Lift.Case 62 MODEL: FunOrn.Lift.Examples.Head

vappend:

  Patch type+ type++ -+ -

  Extension (O : Orn D u) (xs : D (µ E)) : SET -Ask for freshly inserted data, it is the data missing from xs: Extension (insert S D + ) xs → (s : S) × Extension (D + s) xs -Do not duplicate the original data, it is already in xs:

6. 15 ZU064

 15 Definition (Reornament structure65 ). We capture the recursive structure of the reornament by traversing the ornament while peeling off the index xs along the way. The crucial step is the variable case (case var): we ask for a reornament µ ⌈o⌉ orn taken at the index specified by the ornament and the current index xs. The other cases are only creating to cover all the recursive arguments. Structure (O : Orn D u) (xs : D (µ E)) (e : Extension O xs) : SET -Extract the next index from the ornament and the index: Structure (var (inv i)) xs * → µ ⌈o⌉ orn (i, xs) -Duplicate (only) the recursive structure: Structure (insert S D + ) xs (s, e) → Structure (D + s) xs e Structure 1 : S)Structure (T + s) ( f s) (e s) Structure (Σ T + ) (s, xs) e → Structure (T + s) xs e Structure (delete s T + ) (s, xs) (refl, e) → Structure T + xs e DEFINITION ▽ The decomposition of the reornament in terms of an extension and its recursive structure is formally expressed by the following isomorphism: Let D:IDesc I be a description code and let O:Orn D u be an ornament code of D. For all xs : D (µ E), we have: (e : Extension O xs) × Structure O xs e ∼ = ⌈O⌉ orn xs orn (µ o)

  per se, only the recursive structure of the datatype. mkReorn (O : Orn D u) (xs : D (µ E)) (e : Extension O xs) (a : Structure O xs e) : ⌈O⌉ xs orn (µ ⌈o⌉ orn ) mkReorn (insert S D + ) xs (s, e) a → (s, mkReorn (D + s) e a) mkReorn (var (inv i)) xs * a → a mkReorn 1 * * * → * mkReorn (Π T + ) f e a → λs. mkReorn (T + s) ( f s) (e s) (a s) mkReorn (Σ T + ) (s, xs) e a → mkReorn (T + s) xs e a mkReorn (delete s T + ) (s, xs) (refl, e) a → (refl, mkReorn T + xs e a) DEFINITION ▽ 6.17 Definition (Lifting of constructor 67 ). This clear separation of concerns is a blessing for us: when lifting a constructor, we only have to provide the extension and the arguments of the datatype, nothing more. The implementation is as simple as: lift-constructor (e : Extension (o i) xs) -coherent extension (a : Structure (o i) xs e) -recursive arguments (t ++ : Patch T T + t) : Patch (µ{D • u i }× T ) (µ + {o • inv i }× T + ) (in xs,t) lift-constructor e a t ++ → (in (mkReorn (o i) xs e a),t ++ ) DEFINITION For convenience, we extend our high-level notation with a gadget for returning a lifted constructor. We shall therefore write . . . lift → e[a] to denote the low-level term lift-constructor e a * A few examples illustrating this notation follow (Example 6.18 and Example 6.19). ▽ 6.18 Example (Transporting the constructors of isSuc 68 ). Let us finish the implementation of hd from isSuc. Our task is simply to transport the true and false constructors along the Maybe ornament. In a high-level notation, we would write the command shown in Fig. 7(c) (p.55). The interactive system would then respond by generating the code of Fig. 7(d) (p.55). The unit goals are trivially solved. The only information the user has to provide is a value of type A, which is required by the just constructor. △ 67 MODEL: FunOrn.Lift.Constructor 68 MODEL: FunOrn.Lift.Examples.Head Request lifting of algebra (user input): ihd (vs : Vec A n) : IMaybe A (isSuc n) ihd { lift ⇐ lift-fold} (b) Result of lifting the algebra (system output): ihd (vs : Vec A n) : IMaybe A (isSuc n) ihd lift ⇐ lift-fold where ihdAlg (vs : Vec-func (λn ′ . IMaybe A (isSuc n ′ )) n) : IMaybe A (isSuc n) ihdAlg 'nil {?} ihdAlg ('cons a xs) {?} (c) Request lifting of constructors (user input):

Fig

  Fig. 7: Guided implementation of ihd

vappend:

  Patch type+ type++ -+vappend (suc m) (cons a xs) n ys lift → cons {? : A} [ {?} ]Concluding the implementation of vappend is then left to the programmer:vappend : Patch type+ type++ -+ -

  Our work is an extension of the work of McBride (

A→

  Worked example: from comparison to lookup A.1 The comparison function (a) Specify the type of the comparison function: type< : Type type< → µ{Nat-func • * }→ µ{Nat-func • * }→ µ{Bool-func • * }× 1 (b) Implement the comparison function: -< -: type< Type m < n ⇐ Nat-elim n m < 0 → false m < (suc n) ⇐ Nat-case m 0 < (suc n) → true (suc m) < (suc n) → m < n A.2 The functional ornament (a) Specify the ornamented type of the lookup function: typeLookup : FunOrn type< typeLookup → µ + {idO Nat-func • inv * }→ µ + {List-Orn A • inv * }→ µ + {Maybe-Orn A • inv * }× 1 (b) Implement its Patch type: ilookup : Patch type< typeLookup (-< -) ilookup m m + n vs {?} (c) Lift the induction: ilookup : Patch type< typeLookup (-< -)ilookup m m + n vs lift ⇐ lift-ind ilookup m m + 0 nil {?} ilookup m m + (suc n) (cons a vs) {?} (d) Lift the case analysis: ilookup : Patch type< typeLookup (-< -) ilookup (suc m) (suc m + ) just {a : A} [ * ] ilookup (suc m) (suc m + ) (suc n) (cons a vs) {?}(f) Finish the definition:ilookup : Patch type< typeLookup (-< -) n) (cons a vs) lift → just a[ * ] ilookup (suc m) (suc m + ) (suc n) (cons a vs) → ilookup m m + n vsA.3 Extracting the lookup function (a) Obtain the lookup function by applying the patch: lookup : typeLookup FunOrn lookup → patch typeLookup (-< -) ilookup (b) Obtain a proof of its coherence: cohLookup (n : Nat) (xs : List A) : isJust (lookup n xs) = n < length xs cohLookup n xs → coherence typeLookup (-< -) ilookup n xs of descriptions data IDesc [I : SET] : SET 1 where IDescI ∋ var (i : I) | 1 | Π (S : SET) (T : S → IDesc I) | Σ (S : SET) (T : S → IDesc I) (D : IDesc I) (X : I → SET) : SET var i X → X i 1 X → 1 Π S T X → (s : S) → T s X Σ S T X → (s : S) × T s X func (I : SET) : SET 1 func I → I → IDesc I (D : func I) (X : I → SET) : I → SET D X → λi. D i X Code and interpretation data µ [D : func I](i : I) : SET where µ D i ∋ in (xs : D (µ D) i) induction :∀ P : ∀ i : I. µ D i → SET. (α : (i : I)(xs : D (µ D) i) → D P xs → P (in xs)) (x : µ D i) → P x of ornaments data Orn (D : IDesc K)[u : I → K] : SET 1 where -Extend with S: Orn D u ∋ insert (S : SET) (D + : S → Orn D u) -Refine index: Orn (var k) u ∋ var (i : u -1 k) -Copy the original: Orn 1 u ∋ 1 Orn (Π S T ) u ∋ Π (T + : (s : S) → Orn (T s) u) Orn (Σ S T ) u ∋ Σ (T + : (s : S) → Orn (T s) u) -Delete S: | delete (s : S) (T + : Orn (T s) u) (O : Orn D u) orn : IDesc I insert S D + orn → Σ S λs. D + s orn var (inv i) orn → var i 1 orn → 1 Π T + orn → Π S λs. T + s orn Σ T + orn → Σ S λs. T + s orn delete s T + orn → T + orn orn (D : func K) (u : I → K) : SET 1 orn D u → (i : I) → Orn (D (u i)) u (o : orn D u) orn : func I o orn → λi. o i ornCode and interpretationforgetNT :(o : orn D u) → o (X • u) i → D X (u i) forgetAlg : (o : orn D u) → o orn (µ D • u) i → µ D (u i) forget : (o : orn D u) → µ o orn i → µ D (u i)Ornamental algebra(D : func K) (α: D X → X) : orn D (π 0 : (k : K) × X k → K) coherentOrn : (t α : µ D α orn (k, x)) → α (forget D α t α ) = x make (D : func I) (α:∀ i. D X i → X i) : (t : µ D k) → µ D α orn (k, α t) Algebraic ornament ⌈(o : orn D u)⌉ : orn o orn (π 0 : (k : K) × X k → K) of function types data Type : SET 1 where Type ∋ µ{(D : func K) • (k : K) }→ (T : Type) | µ{(D : func K) • (k : K) }× (T : Type) | 1 (T : Type) Type : SET µ{D • k }→ T Type → µ D k → T Type µ{D • k }× T Type → µ D k × T Type 1 Type → 1Code and interpretationB.4 Universe of functional ornamentsdata FunOrn (T : Type) : SET 1 where FunOrn (µ{D• k }→ T ) ∋ ∀ u : I → K. µ + {(o : orn D u) • (i : u -1 k) }→ (T + : FunOrn T ) FunOrn (µ{D • k }× T ) ∋ ∀ u : I → K. µ + {(o : orn D u) • (i : u -1 k) }× (T + : FunOrn T ) FunOrn 1 ∋ 1 (T + : FunOrn T ) FunOrn : SET µ + {o • inv i }→ T + FunOrn → µ o orn i → T + FunOrn µ + {o • inv i }× T + FunOrn → µ o orn i × T + Coherence (T + : FunOrn T ) ( f : T Type ) ( f + : T + FunOrn ) : SET Coherence (µ + {o • inv i }→ T + ) f f + → (x + : µ o orn i) → Coherence T + ( f (forget o x + )) ( f + x + ) Coherence (µ + {o • inv i }× T + ) (x, xs) (x + , xs + ) → forget o x + = x × Coherence T + xs xs + Patch (T : Type) (T + : FunOrn T ) ( f : T Type ) : SET Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) f → (x : µ D (u i)) → µ ⌈o⌉ orn (i, x) → Patch T T + ( f x) Patch (µ{D • u i }× T ) (µ + {o • inv i }× T + ) (x, xs) → µ ⌈o⌉ orn (i, x) × Patch T T + xs Patch Patch patch (T + : FunOrn T ) ( f : T Type ) ( f ++ : Patch T T + f ) : T + FunOrn patch (µ + {o • inv i }→ T + ) f f ++ → λx + . patch T + ( f (forget o x + )) ( f ++ (forget o x + ) (make ⌈o⌉ x + )) patch (µ + {o • inv i }× T + ) (x, xs) (x ++ , xs ++ ) → (forget ⌈o⌉ x ++ , patch T + xs xs ++ ) + : FunOrn T ) ( f : T Type ) ( f ++ : Patch T T + f ) : Coherence T + f (patch T + f f ++ ) coherence (µ + {o • inv i }→ T + ) f f ++ → λx + . coherence T + ( f (forget o x + )) ( f ++ (forget o x + ) (make ⌈o⌉ x + )) coherence (µ + {o • inv i }× T + ) (x, xs) (x + , xs ++ ) → (coherentOrn x + , coherence T + xs xs ++ ) recursion patterns lift Alg (α : ∀ k : K. D (λ -. T Type ) k → T Type ) (o : orn D u) (T + : FunOrn T ) : SET lift Alg α o T + → ∀ (i,t) : (i : I) × µ D (u i). ⌈o⌉ orn (λ(i,t). Patch T T + ( α t)) (i,t) → Patch T T + ( α t) lift-fold (α : ∀ k : K. D (λ -. T Type ) k → T Type ) (α ++ : lift Alg α o T + ) : Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) α lift-fold α α ++ → λx. λx ++ . α ++ x ++Coherent algebra and its liftinglift IH (α : (k : K)(xs : D (µ D) k) → D (λ -. T Type ) xs → T Type ) (o : orn D u)(T + : FunOrn T ) : SET lift IH α o T + → ((i,t) : (i : I) × µ D (u i)) → (xs : ⌈o⌉ orn (µ ⌈o⌉ orn ) (i,t)) →⌈o⌉ orn (λ(i,t). Patch T T + (induction α t)) xs → Patch T T + (induction α t) lift-ind (α : (k : K)(xs : D (µ D) k) → D (λ -. T Type ) xs → T Type ) (α ++ : lift IH α o T + ) : Patch (µ{D • u i }→ T ) (µ + {o • inv i }→ T + ) (induction α) lift-ind α α ++ → λx. λx ++ . induction α ++ x ++ Coherent inductive step and its lifting lift-constructor (e : Extension (o i) xs) -coherent extension (a : Structure (o i) xs e) -recursive arguments (t ++ : Patch T T + t) : Patch (µ{D • u i }× T ) (µ + {o • inv i }× T + ) (in xs,t) lift-constructor e a t ++ → (in (mkReorn (o i) xs e a),t ++ )

  Examples.Maybe 21 MODEL: Orn.Ornament.Examples.List

	ZU064-05-FPR	paper	13 December 2013	17:37
		22		Dagand and McBride
		4.8 Example (Ornamenting natural numbers to finite sets 22

  denotes the catamorphism, which can be implemented in terms of induction[START_REF] Chapman | The gentle art of levitation[END_REF]. ▽4.16Example (From lists back to natural numbers 28 ). Applied to the ornament List-Orn, the Cartesian morphism removes the extra information added through insert, i.e. the inhabitant of A. The resulting algebra thus takes nil to 0, and cons a to suc. In turn, the forgetful map computes the length of the list. We have (automatically) constructed the length function from Section 2. △ From the option type back to Booleans 29 ). Applied to Maybe-Orn, the Cartesian morphism removes the a : A we attached to the constructor true. The forgetful map corresponds exactly to the function isJust (Section 2). △ 4.18 Example (From finite sets back to natural numbers 30 ). Applied to the ornament Fin-Orn, the Cartesian morphism removes the equations introduced by insert and forgets the indexing discipline enforced by the var code. The resulting forgetful map computes the cardinality -a natural number -of a finite set. It corresponds to the following function:

	ZU064-05-FPR	paper	13 December 2013	17:37
		26		Dagand and McBride
		4.17 Example (

  14, we have constructed, for an ornament o, its ornamental algebra forgetAlg o that forgets the extra information introduced by the ornament. As hinted at in Example 4.22, given an ornament o, we can always algebraically ornament o orn using the ornamental algebra forgetAlg o. McBride (2013) calls this construction the algebraic ornament by the ornamental algebra.

4.25 Remark (Notation). We write ⌈o⌉ to denote the algebraic ornament of o by the ornamental algebra. For brevity, we call it the reornament of o. ♦ 4.26 Example (Reornament: vectors). Paraphrasing Example 4.22, we have that vectors are a reornament of List-Orn. Explicitly, a vector is the algebraic ornament of List by the algebra computing its length, i.e. the ornamental algebra from List to Nat. △ 4.27 Example (Reornament: indexed option type). In Example 4.5, we have ornamented the Booleans to the option type. We can thus reornament the option type with its Boolean status. Unfolding the definition of the reornament, we obtain the IMaybe A datatype that was introduced in Section 2. The function forgetIMaybe corresponds to the left-to-right reading of the isomorphism (4.20) specialised to the Maybe ornament. △

  Note that our ability to compute over indices is crucial for this construction to work. Also, the datatypes we obtain are isomorphic to the datatypes one would have obtained by the algebraic ornament of the ornamental algebra, i.e.: Computational interpretation). Consequently, the coherence property of algebraic ornaments (Equation4.20) is still valid. Constructively, this isomorphism gives the coherentOrn theorem 41 in one direction and the make function 42 in the other. ♦4.33 Remark (Iterating reornamentation 43

	ZU064-05-FPR	paper	13 December 2013	17:37
		32		Dagand and McBride
		4.32 Remark (
				META-THEOREM
		For all ornament o : orn D u, we have
			⌈o⌉ orn ∼ =	o orn	forgetAlg o	orn

in xs). ⌈o i⌉ xs DEFINITION ▽ 4.30 Example (Reornament: vectors 39 ). Applied to the ornament List-Orn (Example 4.7), this construction gives the fully Brady-optimised -detagged and forced -version of vectors (Example 3.8). That is, we determine which constructor of Vec is available by patternmatching on the index. This is unlike the naive reornament (Example 4.26), which relies on constraints to enforce the indexing discipline. △ 4.31 Example (Reornament: indexed option type 40 ). Under this definition, the reornament of Maybe-Orn (Example 4.5) describes the datatype data IMaybe [A : SET](b : Bool) : SET where IMaybe A true ∋ just (a : A) IMaybe A false ∋ nothing where, similarly, constraints are off-loaded by pattern-matching on the indices (Example 3.8). Again, this must be compared with the definition obtained through the naive construction (Example 4.27), where we relied on constraints. △ 39 MODEL: Orn.Reornament.Examples.List 40 MODEL: Orn.Reornament.Examples.Maybe

  orn i → µ o E orn j is said to be coherent with f if the following diagram commutes

	ZU064-05-FPR	paper	13 December 2013	17:37
				Functional Ornaments	37
		µ o D

  ⌈o⌉ x ++ , patch T + xs xs ++ ) are introduced (i.e. with the code µ + {o • inv i }→ ), we simply patch the body of the function. This is possible because from x + : µ o D orn , we can

	ZU064-05-FPR	paper	13 December 2013	17:37
					Functional Ornaments
					DEFINITION
			patch	1	*	*	→ *
		When ornamented arguments 54 MODEL: FunOrn.Patch.Apply

  induction α t)

	ZU064-05-FPR	paper	13 December 2013	17:37
				DEFINITION
				▽
		58 MODEL: FunOrn.Lift.Fold
		59 MODEL: FunOrn.Lift.Induction

MODEL: IDesc.IDesc

MODEL: IDesc.IDesc

MODEL: IDesc.IDesc.InitialAlgebra

MODEL: IDesc.IDesc.Induction

MODEL: IDesc.IDesc.Lifting

MODEL: IDesc.Examples.Vec

MODEL: IDesc.Examples.Fin

MODEL: IDesc.Examples.Vec

MODEL: IDesc.Examples.STLC

MODEL: IDesc.Examples.Id

MODEL: Orn.Ornament

MODEL: Orn.Ornament

MODEL: Orn.Ornament.Examples.Fin

MODEL: Orn.Ornament.Identity

MODEL: Orn.Ornament.Examples.Vec

MODEL: Orn.Ornament.Examples.Fin

MODEL: Orn.Ornament.Algebra

MODEL: Orn.Ornament.Examples.List

Keeping with standard notations, we denote refinement types with a set comprehension. In type theory, this amounts to a Σ-type.

MODEL: Orn.AlgebraicOrnament.Coherence

MODEL: Orn.AlgebraicOrnament.Make

MODEL: Orn.AlgebraicOrnament.Examples.Vec

MODEL: FunOrn.FunOrnament

MODEL: FunOrn.FunOrnament

MODEL: FunOrn.FunOrnament.Examples.Lookup

MODEL: FunOrn.Patch.Coherence

MODEL: FunOrn.Lift.Examples.Lookup

MODEL: FunOrn.Lift.Examples.Append

MODEL: FunOrn.Lift.Examples.Lookup

MODEL: FunOrn.Lift.Examples.Append

MODEL: FunOrn.Lift.MkReorn

MODEL: FunOrn.Lift.MkReorn

MODEL: FunOrn.Lift.Examples.Lookup

MODEL: FunOrn.Lift.Examples.Append

Acknowledgements We owe many thanks to the ICFP and JFP reviewers, their comments having significantly improved this article. We are also very grateful to Guillaume Allais, Stevan Andjelkovic and Peter Hancock for their meticulous reviews of this paper. We shall also thank Edwin Brady for suggesting the study of lookup functions and Andrea Vezzosi for spotting an issue in our definition of reornaments. Finally, this paper would have remained a draft without the help and encouragement of José Pedro Magalhães. The authors are supported by the Engineering and Physical Sciences Research Council, Grant EP/G034699/1. ZU064-05-FPR paper 13 December 2013 17:37

Functional Ornaments