Transporting Functions across Ornaments
Technical Report

arXiv:1201.4801v2 [] 12 Mar 2012

Pierre-Evariste Dagand

Conor McBride

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 effort of code reuse among similarly structured data. In this
paper, we exorcise our datatypes by adapting 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 ornament, 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.

1 Introduction
Imagine designing a library for a 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 optimised set
of operations. If, tempted by a snake, we move to a language with richer datatypes,
such as a dependently typed 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 the ML days, datatypes have evolved: besides providing an organising structure
for computation, they are now offering more control over what is a valid result. With

1

richer datatypes, the programmer can enforce invariants on top of the data-structures.
In such a system, programmers strive to express the correctness of programs in their
types: a well typed program is correct by construction, the proof of correctness being
reduced to type-checking.
A simple yet powerful recipe to obtain these richer datatypes is to index the datastructure. These datatypes have originally been studied in the context of type theory under the name of inductive families [Dybjer, 1994, Morris et al., 2009]. Inductive families made it to mainstream functional programming with Generalised Algebraic
Data-Types [Cheney and Hinze, 2003, Xi et al., 2003], a subset of inductive families for
which type inference remains decidable. Refinement types [Freeman and Pfenning, 1991,
Swamy et al., 2011] are another technique to equip data-structures with rich invariants.
Atkey et al. [2011] have shown how refinement types relate to inductive families, and
Bernardy and Lasson [2011] establish a connection with realisability.
However, these carefully crafted datatypes are a threat to any library design: the same
data-structure is used for logically incompatible purposes. This explosion of specialised
datatypes is overwhelming: these objects are too specialised to fit in a global library.
Yet, because they share this common structure, many operations on them are extremely
similar, if not exactly the same. To address this issue, McBride developed ornaments,
describing how one datatype can be enriched into others with the same structure. Such
structure-preserving transformations take two forms: one can extend the initial type
with more information – such as obtaining MaybeA from Bool or ListA from Nat:
data Bool : Set where
Bool ∋ true
| false
data Nat : Set where
Nat ∋ 0
| suc (n : Nat)

Maybe-Orn

=⇒

List-Orn

=⇒

data Maybe [A : Set] : Set where
MaybeA ∋ just (a : A)
| nothing
data List [A : Set] : Set where
ListA ∋ nil
| cons (a : A)(as : ListA )

Or one can refine the indexing of the initial type by a finer discipline – e.g., obtaining
Fin by indexing Nat with a bound n:
data Nat : Set where
Nat ∋ 0
| suc (n : Nat)

data Fin (n : Nat) : Set where
=⇒
Fin (n = suc n ′ ) ∋ f0 (n ′ : Nat)
| fsuc (n ′ : Nat)(fn : Fin n ′ )

Fin-Orn

One can also do both at the same time – such as extending Nat into a ListA while
refining the index to match the length of the list:
data Nat : Set where
Nat ∋ 0
| suc (n : Nat)

data Vec [A : Set](n : Nat) : Set where
=⇒
VecA (n = 0) ∋ nil
VecA (n = suc n ′ ) ∋ cons (n ′ : Nat)(a : A)(vs : VecA n ′ )

Vec-Orn

Note that we declare datatype parameters [A : Set] in brackets and datatype indices
(n : Nat) in parentheses. We make equational constraints on the latter only when needed,
and explicitly.

2

Because of their constructive nature, ornaments are not merely identifying similar
structures: they give an effective recipe to build new datatypes from old, guaranteeing
by construction that the structure is preserved. Hence, we can obtain a plethora of new
datatypes with minimal effort.
Whilst we now 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 ListA as an ornament of Nat, it seems natural to transport
some structure-preserving function of Nat to ListA , such as moving from addition of
natural numbers to concatenation of lists:
(m : Nat) + (n : Nat) : Nat
(xs : ListA ) ++ (ys : ListA ) : ListA
0
+
n
7→ n
++
ys
7→ ys
⇒ nil
(suc m) +
n
7→ suc (m + n)
(cons a xs) ++
ys
7→ cons a (xs ++ ys)
(m : Nat) − (n : Nat)
0
−
n
m
−
0
(suc m) − (suc n)

:
7→
7
→
7
→

Nat
0
m
m −n

drop (xs : ListA ) (n : Nat)
drop
nil
n
⇒
drop
xs
0
drop (cons a xs) (suc n)

:
7→
7
→
7
→

ListA
nil
xs
drop xs n

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 adapt ornaments to our universe of datatypes [Chapman et al., 2010] in Section 3. This presentation benefits greatly from our ability to inspect indices when
defining datatypes. This allows us to consider ornaments which delete indexdetermined information, yielding a key simplification in the construction of an
algebraic ornament from an ornamental algebra ;
• We describe how functions can be transported through functional ornaments: ‘deletion’ allows us a contrasting approach to Ko and Gibbons [2011], internalising
proof obligations. First, we manually work through an example in Section 2.
Then, we formalise the concept of functional ornament by a universe construction
in Section 4. Based on this universe, we establish the connection between a base
function (such as + and − ) 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 constructions ;
• In Section 5, we provide further support to drive the computer into lifting functions
semi-automatically. As we can see from our examples above, the lifted functions
often follow the same recursion pattern and return similar constructors: with a few
constructions, we shall remove further clutter and code duplication in our libraries.

3

(m : Nat) < (n : Nat)
m
<
0
0
< suc n
< suc n
suc m

:
7→
7
→
7
→

Bool
lookup (m : Nat) (xs : ListA )
false
m
nil
? lookup
=⇒
true
lookup
0
(cons a xs)
m <n
lookup (suc n) (cons a xs)

:
7
→
7→
7
→

MaybeA
nothing
just a
lookup n xs

Figure 1: Implementation of < and lookup
• Finally, we add a generic gadget to our reusability kit in Section 6: we show how a
careful use of an adjunction can absorb computation at the index-level – which are
notoriously difficult to deal with – and replace them by a special-purpose indexed
family – which is much easier to deal with.
This paper is an exercise in constructive mathematics: upon identifying an isomorphism, we shall look at it with our constructive glasses and obtain an effective procedure
that lets us cross the isomorphism.
We shall write our code in a syntax inspired by the Epigram McBride and McKinna
[2004] programming language. In particular, we make use of the by ( ⇐ ) and return
( 7→ ) 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. Like ML, unbound variables in type definitions are
universally quantified, further abating syntactic noise. The syntax of datatype definitions
draws upon the ML tradition as well: its novelty will be presented by way of examples
in Section 3. All the constructions presented in this paper have been modelled in Agda,
using only standard inductive definitions and two levels of universes. The formalisation
is available on Dagand’s website.

2 From < to lookup, manually
There is an astonishing resemblance between the comparison function < on natural
numbers and the list lookup function (Fig. 1). Interestingly, the similarity is not merely
at the level of types but also in their implementation: their definitions follow the same
pattern of recursion (first, case analysis on the second element; then induction on the
first element) and they both return a failure value (false and nothing respectively) in the
first case analysis and a success value (true and just respectively) 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

4

each individual datatype has been promoted when going from < to lookup:
:

<

→

Nat
idONat

:

lookup

Nat

List-Orn
→

Nat

ListA

→

Bool

Maybe-Orn
→

MaybeA

Note that the first argument is ornamented to itself, or put differently, it has been
ornamented by the identity ornament.
Each of these ornaments come with a forgetful map, computed from the ornamental
algebra:
length (as : ListA ) : Nat
isJust (m : MaybeA ) : Bool
length
nil
7→ 0
isJust nothing
7→ false
length (cons a as) 7→ suc (length as) isJust (just a)
7→ true
Using these forgetful map, the relation, at the computational level, between < and
lookup is uniquely established by following the ornamentation of their types. This relation is naturally expressed by the following coherence property:
∀n : Nat.∀xs : ListA . isJust (lookup n xs) ≡ n < length xs
Or, equivalently, using a commuting diagram:
Nat

×

ListA

lookup

length
Nat

×

MaybeA
isJust

Nat

<

Bool

Let us settle the vocabulary at this stage. 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
(here, Nat → ListA → MaybeA ). A function inhabiting this type is called a lifting (here,
lookup). A lifting is said to be coherent if it satisfies the coherence property. 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 different coherence
properties.
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: one would implement
lookup and prove the coherence as a theorem. This works rather well in a system like

5

Coq [The Coq Development Team] as it offers a powerful theorem proving environment.
It does not work so well in a system like Agda [Norell, 2007] that does not offer tactics to
its users, forcing them to write explicit proof terms. It would not work at all in Haskell
with GADTs, as it does not have any theorem proving capability.
However, we are not satisfied by this laborious approach: if we have dependent types,
why should we use them only for proofs, as an afterthought? We should rather write
a lookup function correct by construction: by implementing a more precisely indexed
version of lookup, the user can drive the index-level computations to unfold, hence making
the type-checker verify the necessary invariants. We believe that this is how it should
be: computers should replace proofs by computation; humans should drive computers.
The other way around – where humans are coerced into computing for computers – may
seem surreal, yet it corresponds to the current situation in most proof systems.
To get the computer to work for us, we would rather implement the function ilookup:
ilookup (m : Nat) (vs : VecA n)
ilookup
m
nil
ilookup
0
(cons a vs)
ilookup (suc m) (cons a vs)

:
7→
7→
7→

IMaybeA (m < n)
nothing
just a
ilookup m vs

Where IMaybeA is MaybeA indexed by its truth as computed by isJust. It is defined as
follows1 :
data IMaybe [A : Set](b : Bool) : Set where
IMaybeA true ∋ just (a : A)
IMaybeA false ∋ nothing
This comes with the following forgetful map2 :
forgetIMaybe (mba : IMaybeA b) : (ma : MaybeA ) × isJust ma ≡ b
forgetIMaybe
(just a)
7→ (just a, true ≡ true) 
forgetIMaybe
nothing
7→ nothing, false ≡ false
The rational behind ilookup is to index the types of lookup by their unornamented
version, i.e. the types of < . Hence, we can make sure that the result computed by
ilookup respects the output of < on the unornamented indices: the result is 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. Expounding further our vocabulary, we call coherent liftings these finely indexed functions that
are correct by construction.
Ko and Gibbons [2011] use ornaments to specify the coherence requirements for functional liftings, but we work the other way around, using ornaments to internalise coherence requirements. From ilookup, we can extract both lookup and its proof of correctness
1

Note that we have overloaded the constructors of Maybe and IMaybe: for a bi-directional type-checker,
there is no ambiguity as constructors are checked against their type.
2
We depart slightly from the convention of calling refl the inhabitant of the identity type a ≡ b: instead
we shall denote it a ≡ b, hence being explicit about which equation is being proved.

6

without having written any proof term ourselves:
lookup (m : Nat) (xs : ListA ) : MaybeA
lookup
m
xs
7→ π0 (forgetIMaybe (ilookup m (makeVec xs)))
cohLookup (n : Nat) (xs : ListA ) : isJust (lookup n xs) ≡ n < length xs
cohLookup
m
xs
7→ π1 (forgetIMaybe (ilookup m (makeVec xs)))
Where makeVec simply turns a list into a vector of the corresponding length.
As a side comment, remark that the function ilookup is very similar to the more
familiar vlookup function:
vlookup (m : Fin n) (vs : VecA n) : A
vlookup
∅
nil
vlookup
f0
(cons a xs) 7→ a
vlookup (fsuc n) (cons a xs) 7→ vlookup n xs
As we shall see later in Section 6, these two definitions are actually isomorphic, thanks
to the following equivalence:
(m : Nat) → IMaybeA (m < n) ∼
= Fin n → A
Intuitively, we can move the constraint that m < n from the result – i.e. IMaybeA (m < n)
– to the premises – i.e. Fin n. This matches our intuition that
Fin n ∼
= (m : Nat) × m < n
Hence, having implemented ilookup, not only do we obtain lookup and its coherence
proof, but we also get the traditional vlookup function.
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 desired lifting, here lookup : Nat → ListA → MaybeA
satisfying ∀n : Nat.∀xs : ListA . isJust (lookup n xs) ≡ n < length xs
• Implement a carefully indexed version of the lifting, here ilookup : (m : Nat)(vs :
VecA n) → IMaybeA (m < n)
• Derive the lifting, here lookup, and its coherence proof, without proving any theorem
Besides, the implementation of ilookup is not lost: this function corresponds exactly to
vector lookup, a function that one would have implemented anyway.
This manual unfolding of the lifting is instructive: it involves a lot of constructions
on datatypes (here, the datatypes ListA and MaybeA ) 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 the next Section, we shall build the
machinery to describe these constructions and obtain them within the type theory itself.

7

data IDesc [I : Set] : Set1 where
IDesc I ∋ ’var (i : I )
| ’1
| ’Π (S : Set) (T : S → IDesc I )
| ’Σ (S : Set) (T : S → IDesc I )

J(D : IDesc I )K (X : I → Set) : Set
J’var i K X 7→ X i
J’1K X
7→ 1
J’Π S T K X 7→ (s : S ) → JT sK X
J’Σ S T K X 7→ (s : S ) × JT sK X

Figure 2: Universe of inductive families

3 A universe of datatypes and their ornaments
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 datatypes 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 datatype definitions, as they belong to the
meta-theory.

3.1 A closed theory of datatypes
In our previous work [Chapman et al., 2010], we have shown how to internalise inductive families into type theory. The practical impact of this approach is that we can
manipulate datatype declarations as first-class objects. We can program over datatype
declarations and, in particular, we can compute new datatypes from old. This is particularly useful to formalise the notion of ornament entirely within the type theory. This
also has a theoretical impact: we do not need to prove meta-theoretical properties of our
constructions, we can work in our type theory and use its logic as our formal system.
Note that our results are not restricted to this setting where datatype definitions
are internalised: all our constructions could be justified at the meta-level and then
be syntactically presented in a language, such as, say, Agda or Haskell with GADTs.
Working with an internalised presentation, we can simply avoid these two levels of logic
and work in the logic provided by the type theory itself.
For the sake of completeness, let us recall a few definitions and results from our
previous work. As in previous work, our requirement on the type theory are minimal:
we will need Σ-, Π-types, and at least two universes. For convenience, we require a
type of finite sets, which lets us build collections of labels3 . We also need a pre-existing
notion of propositional equality, upon which we make no assumption. We internalise the
inductive families by a universe construction (Fig. 2): an indexed datatype is described
by a function from its index to codes. The codes are then interpreted to build the
3

We denote finite sets of tagged elements by {’x, ’y, ’z, . . .}. Their elimination principle consists of
an exhaustive case enumeration and is denoted by {’x 7→ vx, ’y 7→ vy, ’z 7→ vz, . . .}. If the tags are
vertically aligned, we shall skip the separating comma.

8

fix-point:
data µ [D : I → IDesc I ](i : I ) : Set where
µ D i ∋ in (xs : JD i K (µ D))
Inductive types are eliminated by a generic elimination principle:
iinduction : (D : IDesc I )(P : µ D i → Set)
(is : (i : I )(xs : JD i K (µ D)) → iAll D P xs → P (in xs))
(x : µ D i ) → P x
Where, intuitively, iAll D P xs enforces that all sub-trees of xs satisfy P : this corresponds
exactly to computing the inductive hypothesis necessary to perform the induction step.
In the categorical literature [Hermida and Jacobs, 1998, Atkey et al., 2011], iAll D is
denoted D̂.
For readability purposes, we use an informal notation to declare datatypes. This notation is strongly inspired by Agda’s datatype declarations. Note that these definitions
can always be turned into IDesc codes: when defining a datatype T , we will denote
T -Desc the code it elaborates to. Similarly, we denote T -elim and T -case the induction
principle and case analysis operators associated with T . These operations can be implemented by generic programming, along the lines of McBride et al. [2004]. Formalising
the elaboration of datatypes definitions down to code is beyond the scope of this paper.
However, it is simple enough to be understood with a few examples. Three key ideas
are at play.
First, non-indexed datatypes definitions follow the ML tradition: we name the datatype
and then comes a choice of constructors. For example, List would be written and elaborated as follows:
data List [A : Set] : Set where
ListA ∋ nil
| cons (a : A)(as : ListA )
λA. λ∗.
’Σ



’nil
’cons



’nil →
7 ’1
’cons →
7 ’Σ A λ . ’var ∗

Secondly, indexed datatypes can be defined following the Agda convention: indices
are constrained to some particular value. For example, Vec could be defined by con-

9

straining the index to be 0 in the nil case and suc n′ for some n′ : Nat in the cons case:
data Vec [A : Set](n : Nat) : Set where
VecA (n = 0) ∋ nil
VecA (n = suc n ′ ) ∋ cons (n ′ : Nat)(a : A)(vs : VecA n ′ )


’vnil
λA. λn. ’Σ
 ’vcons
’vnil 7→ ’Σ (n ≡ 0) λ . ’1
’vcons 7→ ’Σ Nat λn ′ . ’Σ (n ≡ suc n ′ )λ .

’Σ A λ . ’var n ′





The elaboration naturally captures the constraints on indices by using propositional
equality. In the case of Vec, we abstract over the index n, introduce the choice of
constructors with the first ’Σ and, once constructors have been chosen, we restrict n to
its valid value(s): 0 in the first case and suc n′ for some n′ in the second case.
Thirdly, we can compute over indices: here, we make use of the crucial property that
a datatype definition is a function from index to IDesc codes. Hence, our notation should
reflect this ability to define datatypes as functions on their index. For instance, inspired
by Brady et al. [2004], an alternative presentation of vector would match on the index
to determine the constructor to be presented, hence removing the need for constraints:
data Vec [A : Set](n : Nat) : Set where
n
VecA
⇐ Nat-case n
VecA 0
∋ nil
VecA (suc n) ∋ cons (a : A)(vs : VecA n)
λn.
Nat-case n (λ . IDesc Nat)
’1
(λn. ’Σ A λ . ’var n)
In order to be fully explicit about computations, we use here the Epigram [McBride and McKinna,
2004] by ( ⇐ ) programming gadget, which let us appeal to any elimination principle
with a syntax close to pattern-matching. However, standard pattern-matching constructions [Coquand, 1992, Norell, 2007] would work just as well. Again, we shall write
pattern-matching definitions when the recursion pattern is unremarkable.
Our syntax departs radically from the one adopted by Coq, Agda, and GADTs in
Haskell. It is crucial to understand that this is but reflecting the actual semantics of
inductive families: we can compute over indices, not merely constrain them to be what
we would like. 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.

10

As a final example, let us look at the datatype of infinite staircase walks: at each
step, we can unconditionally go up. Besides, after pattern-matching on the index, we
can decide to stop on step 0 and, for any non-zero step, we can also go down:
data Walk (n : Nat) : Set where
Walk n
∋ up (w : Walk (suc n))
Walk 0
∋ stop
Walk (suc n) ∋ down (w : Walk n)

Remark: Note that we have been careful in using equality to introduce constraints here:
our definition of datatypes is absolutely agnostic in the notion of equality assumed 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. Concretely, the standard definition of the
identity types is presented and elaborated as follows:
data Id [a1 : A](a2 : A) : Set where
Id a1 (a2 = a1 ) ∋ refl
λa1 a2 .
’Σ {’refl}{’Σ (a2 ≡ a1 )λ . ’1}
We have been careful to maintain our presentation of ornaments and functional ornaments similarly equality agnostic.

3.2 Ornaments
Originally, McBride presented the notion of ornament for a universe where the indices a
constructor targets could be enforced only by equality constraints. As a consequence, in
that simpler setting, computing types from indices was impossible. We shall now adapt
the original definition to our setting.
Just as the original definition, an ornament is defined upon a base datatype – specified
by a function D : I → IDesc I – and indices are refined up to a reindexing function
re : J → I. The difference in our setting is that, just as the code of datatypes can
be computed from the indices, we want the ornament to be computable from its Jindex. Hence, an ornament is a function from j : J to ornament codes describing the
ornamentation of D (re j):
orn (re : J → I ) (D : I → IDesc I ) : Set1
orn
re
D
7→ (j : J ) → Orn re (D (re j ))
As for the ornament codes themselves, they are similar to the original definition: we
shall be able to copy the base datatype, extend it by inserting sets, or refine the indexing subject to the relation imposed by re. However, we also have the J-index in

11

our context: following Brady’s insight that inductive families need not store their indices [Brady et al., 2004], we could as well delete parts of a datatype definition as long
as we can recover the suppressed bits from the index. Hence, we obtain the following
code4 :
data Orn [re : J → I ](D : IDesc I ) : Set1 where
– Extend with S:
Orn re
D
∋ insert (S : Set)(D + : S → Orn re D)
D
⇐ IDesc-case D
Orn re
– Refine index:
Orn re (’var i ) ∋ ’var (j : re −1 i )
– Copy original:
Orn re
’1
∋ ’1
Orn re (’Π S T ) ∋ ’Π (T + : (s : S ) → Orn re (T s))
Orn re (’Σ S T ) ∋ ’Σ (T + : (s : S ) → Orn re (T s))
– Delete S:
| delete (replace : S )(T + : Orn re (T replace))
Given an ornament, we can interpret it as the datatype it describes. The implementation consists in traversing the ornament code, introducing a ’Σ when inserting new
data and computing the ornament at the replaced value when deleting some redundant
data:
J(o : orn re D)Korn (j : J ) : IDesc J
JoKorn
j
7→ intOrn (D (re j )) (o j )
where
intOrn (D : IDesc I ) (O : Orn re D)
intOrn
D
insert S D +
intOrn (’var (re j ))
(’var (inv j ))
intOrn
’1
’1
intOrn (’Π S T )
(’Π T + )
intOrn (’Σ S T )
(’Σ T + )
intOrn (’Σ S T ) (delete replace T + )

:
7
→
7
→
7→
7→
7→
7
→

IDesc J
’Σ S λs. intOrn D (D + s)
’var j
’1
’Π S λs. intOrn (T s) (T + s)
’Σ S λs. intOrn (T s) (T + s)
intOrn (T replace) (T + replace)

Note that in the delete case, no ’Σ code is generated: the set S has been deleted from
the original datatype. The witness of this existential is instead provided by replace.
Once again, we adopt an informal notation to describe ornaments conveniently. The
idea is to simply mirror our data definition, adding from which datatype the ornament
is defined. When specifying a constructor, we can then extend it with a new element
using [s : S] or delete an element originally named s by giving its value with [s , value].
Some typical examples of extension are presented in Figure 3.
4

The inverse image of a function is defined by:
data (−1 ) [f : A → B ](b : B) : Set where
f −1 (b = f a) ∋ inv (a : A)

12

data List [A : Set] from Nat where
ListA ∋ nil
| cons [a : A](as : ListA )
data Vec [A : Set](n : Nat) from ListA where
VecA n ∋ nil [q : n ≡ 0]
| cons [n ′ : Nat][q : n ≡ suc n ′ ](a : A)(vs : VecA n ′ )
data Fin (n : Nat) from Nat where
Fin n ∋ f0 [n ′ : Nat][q : n ≡ suc n ′ ]
| fsuc [n ′ : Nat][q : n ≡ suc n ′ ](fn : Fin n ′ )
Figure 3: Examples of ornament
While the definition Vec in Figure 3 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:
data Vec [A : Set](n : Nat) from ListA where
VecA
0
∋ nil
′
VecA (suc n ) ∋ cons (a : A)(vs : VecA n ′ )
Note that such a definition was unavailable in the basic presentation [McBride]. Brady et al.
[2004] call this operation detagging: the constructors of the datatype are determined by
the index. The definition of Fin given in Figure 3 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 deleting the resulting, obvious proof. Hence, Fin can be further ornamented to the optimised Fin’, which makes crucial use of deletion:
data Fin’ (n : Nat) from Fin where
Fin’ 0
∋ [b : 0](0-elim b)
– no constructor
Fin’ (suc n) ∋ f0 [n ′ , n][q , n ≡ n]
| fsuc [n ′ , n][q , n ≡ n](fn : Fin’ n ′ )
Again, this definition was previously unavailable to us. Besides, we are making crucial
use of the deletion ornament to avoid duplication. Brady et al. [2004] call this operation
forcing: the content of the constructors, here n′ and the constraint, are computed from
the index.
Just as the datatype declaration syntax was elaborated to IDesc codes, this high-level
syntax is elaborated to ornament codes. The formal description of this translation is
beyond the scope of this paper. From the definition of an ornamented type T , we will
assume the existence of its corresponding ornament code T -Orn.
As described by McBride, every ornament induces an ornamental algebra: intuitively,
an algebra that forgets the extra data, hence mapping the ornamented datatype back to
its unornamented form. From an ornament O : orn reD, there is a natural transformation

13

from the ornamented functor down to the unornamented one, which we denote:
O-forgetNat : (X : I → Set)(j : J ) → JJO Korn j K (X ◦ re) → JD (re j )K X
Applied with µ D for X and post-composed with in, this natural transformation induces
the ornamental algebra:
O-forgetAlg : (j : J ) → JJO Korn j K (µ D ◦ re) → µ D (re j )
In turn, this algebra induces an ornamental forgetful map denoted:
O-forget : (j : J ) → µ JOKorn j → µ D (re j )
We do not re-implement these functions here: it is straightforward to update the original
definitions to our setting.
3.2.1 Algebraic ornaments
An important class of datatypes is constructed by algebraic ornamentation over a base
datatype. The idea of an algebraic ornament is to index an inductive type by the result
of a fold over the original data: from the code D : I → IDesc I and an algebra α : (i :
I) → JD i K X → X i , there is an ornament that defines a code D α : (i : I) × X i → IDesc (i :
I) × X i with the property that:
µ D α (i, x) ∼
= (t : µ D i) × LαM t ≡ x
We shall indiscriminately use D α to refer to the ornament and the resulting datatype.
Seen as a refinement type, the correctness property states that µ D α (i, x) ∼
= {t ∈
α
µ D i | LαM t = x}. The type theoretic construction of D is described by McBride.
We shall not reiterate it here, the implementation being essentially the same for our
universe. A categorical presentation was also given in Atkey et al. [2011] in which the
connection with refinement types was explored.
Constructively, the correctness property gives us two (mutually inverse) functions.
The direction µ D α (i, x) → (t : µ D i) × LαM t ≡ x relies on the generic D α -forget function
to compute the first component of the pair and gives us the following theorem:
coherentOrn : ∀t α : µ D α (i , x ). LαM (D α -forget t α ) ≡ x
This corresponds to the Recomputation theorem of McBride. We shall not reprove it
here, the construction being similar. In the other direction, the isomorphism gives us a
function of type:
(t : µ D i) × LαM t ≡ x → µ D α (i, x)
Put in full and simplifying the equation, this corresponds to the following function:
D α -make : (t : µ D i ) → µ D α (i , LαM t)
This corresponds to the remember function of McBride. Again, we will assume this
construction here.

14

3.2.2 Reornaments
In this paper, we are interested in a special sub-class of algebraic ornaments. As we
have seen, every ornament O induces an ornamental algebra O-forgetAlg, which forgets
the extra information introduced by the ornament. Hence, given a datatype D and an
ornament OD of D, we can algebraically ornament JOD Korn using the ornamental algebra
OD -forgetAlg. We denote the resulting ornament D OD .
McBride calls this object the algebraic ornament by the ornamental algebra. For
brevity, we call the object D OD the reornament of OD . Again, we shall overload D OD to
denote both the ornament and the resulting datatype. A standard example of reornament
is Vec: it is the reornament of List-Orn. Put otherwise, a vector is the algebraic ornament
of List by the algebra computing its length, i.e. the ornamental algebra from List to Nat.
Reornaments can be implemented straightforwardly by unfolding their definition: 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.
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 Vec reornament would be as follows:
• We retrieve the index, hence obtaining n ;
• By inspecting the ornament List-Orn, we obtain exactly the information by which
n is extended into a list: if n = 0, no supplementary information is needed and if
n = suc n′ , we need to extend it with an a : A. We call this the Extension of n ;
• By inspecting the ornament List-Orn again, we obtain the recursive structure of
the reornament by deleting the data already fully determined by the index and its
extension, and refining the indexing discipline: the tail of a vector of size suc n′ is
a vector of size n′ . The recursive structure is denoted by Structure.
Let us formalise this intuition for any ornament. By the coherence property, we
know that for any index t : µ D, the reornament t++ : µ D OD t is isomorphic to the
comprehension {t + : µ JOKorn j | O-forget t + = t}. Note that the equality constraints are
introduced only to ensure that t+ is built from t through the ornament. Now, in our
setting, we could enforce this constraint by construction: from the ornament OD and
t, we can compute the set of valid extensions of t giving a t+ such that forgetting the

15

extension gives t back:
Extension (O : Orn re j D) (xs : JDK µ D )
Extension
(’var(inv j ))
t
Extension
’1
∗
Extension
(’Π T + )
f
Extension
(’Σ T + )
(s, xs)
Extension (insert S D + )
xs
Extension (delete replace T + )
(s, xs)

:
7
→
7→
7
→
7
→
7
→
7
→

Set
1
1
(s : S ) → Extension (T + s) (f s)
Extension (T + s) xs
(s : S ) × Extension (D + s) xs
(q : s ≡ replace j ) × Extension T + xs

The next step consists in building the recursive structure of the reornamented type.
Again, the recursive structure is entirely described by the ornament together with the
index t: the ornament gives the recursive structure of t+ while the index t specify the
indexing strategy of the sub-nodes: sub-nodes of t++ must be indexed by the corresponding sub-nodes of t. Hence, we obtain the recursive structure of t++ by traversing
the ornament definition while unfolding t along the way in order to reach its sub-nodes.
On a variable, we index by the value specified by the ornament and the t sub-node we
have reached. On a ’Σ and insert, we can delete them to avoid information duplication:
the information is already provided by the index in the case of ’Σ and by the extension
in the case of insert. The formal definition is as follows:
Structure (O : Orn re j D)(xs : JDK µ D)(e : Extension O xs) : Orn π0 (j , t) JO Korn
∗ 7→ ’var (inv (j , t))
Structure (’var (inv j )) t
Structure
’1
∗
∗ 7→ ’1
+
Structure (’Π T )
f
e 7→ ’Π λs. Structure (T + s) (f s) (e s)
+
Structure (’Σ T ) (s, xs) e 7→ delete s (Structure (T + s) xs e)
Structure (insert S D + ) xs (s, e) 7→ delete s (Structure (D + s) xs e)
Structure (delete replace T + ) (replace, xs) s ≡ replace, e 7→ Structure T + xs e

A reornament is thus the Extension of its index followed by the recursive structure as
defined by Structure. Thus, we define the associated reornament at index t = in xs : µ D
by, first, inserting the valid extensions of t with Extension, then, building the recursive
structure using Structure:
reornament (O : orn re D) : orn π0 JOKorn
reornament O 7→ λ(j , in xs). insert (Extension (O j ) xs) λe.
Structure (O j ) xs e
Applied to the reonarment of List-Orn, this construction gives the fully Brady-optimised
– detagged and forced – version of Vec, here written in full:
data Vec [A : Set](n : Nat) : Set where
VecA 0
∋ nil
VecA (suc n) ∋ cons (a : A)(vs : VecA n)
Note that our ability to compute over the index is crucial for this construction to
work. Also, it is isomorphic to the datatype one would have obtained with the algebraic

16

ornament of the ornamental algebra. Consequently, the correctness property of algebraic
ornaments is still valid here: constructively, we get the coherentOrn theorem in one
direction and the ∗-make function in the other direction.
In this Section, we have adapted the notion of ornament to our universe of datatypes.
In doing so, we have introduced the concept of a deletion ornament, using the indexing
to remove duplicated information in the datatypes. This has proved useful to simplify
the definition of reornaments. We shall see how this can be turned to our advantage
when we transport functions across ornaments.

4 A universe of functions and their ornaments
We are now going to generalise the notion of ornament to functions. In order to do this,
we first need to be able, in type theory, to manipulate functions and especially their
types. Hence, we define a universe of functions. With it, we will be able to write generic
programs over the class of functions captured by our universe.
Using this technology, we define a functional ornament as a decoration over the universe of functions. 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: a patch is the type
of the functions that satisfy the coherence property by construction. Finally, and still
writing generic programs, we show how we can automatically project the lifting and its
coherence certificate out of a patch.

4.1 A universe of functions
For clarity of exposition, we restrict our language of types to the bare minimum: a type
can either be an exponential which domain is an inductive object, or a product which
first component is an inductive object, or the unit type – used as a termination symbol:
data Type : Set1 where
Type ∋ µ{(D : I → IDesc I ) (i : I ) }→ (T : Type)
| µ{(D : I → IDesc I ) (i : I ) }× (T : Type)
| 1
Hence, 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:
J(T : Type)KType
Jµ{D i }→ T KType
Jµ{D i }× T KType
J1KType

:
7→
7
→
7
→

Set
µ D i → JT KType
µ D i × JT KType
1

The constructions we develop below could be extended to a more powerful universe
– such as one supporting non-inductive sets or having dependent functions and pairs.
However, this would needlessly complicate our exposition.

17

Example 1 (Coding < ). Written in the universe of function types, the type of <
is:
type< : Type
type< 7→ µ{Nat-Desc ∗ }→ µ{Nat-Desc ∗ }→ µ{Bool-Desc ∗ }× 1
The implementation of < is essentially the same as earlier, excepted that it must
now return a pair of a boolean and an inhabitant of the unit type. To be explicit
about the recursion pattern of this function, we make use of Epigram’s by ( ⇐ ) construct [McBride and McKinna, 2004]:
<
< n
< 0
m
m
< suc n
0
< suc n
suc m < suc n

m

:
⇐
7
→
⇐
7
→
7
→

Jtype<KType
Nat-case n
(false, ∗)
Nat-elim m
(true, ∗)
m <n

That is to say: we first do a case analysis on n and then, in the successor case, we
proceed by induction over m.
Example 2 (Coding + ). Written in the universe of function types, the type of +
is:
type+ : Type
type+ 7→ µ{Nat-Desc ∗ }→ µ{Nat-Desc ∗ }→ µ{Nat-Desc ∗ }× 1
Again, up to a multiplication by 1, the implementation of + is left unchanged:
m

+
+n
0
+n
suc m + n

:
⇐
7
→
7
→

Jtype+KType
Nat-case m
(n, ∗)
(suc m + n, ∗)

4.2 Functional ornament
From the universe of function types, it is now straightforward to define the notion of
functional ornament: we traverse the type and ornament the inductive types as we
go. Note that it is always possible to leave an object unornamented: we ornament by
the identity that simply copies the original definition. Hence, we obtain the following
definition:
data FunOrn (T : Type) : Set1 where
FunOrn (µ{D i }→ T ) ∋ µ+{(O : orn re D) (j : re −1 i ) }→ (T + : FunOrn T )
FunOrn (µ{D i }× T ) ∋ µ+{(O : orn re D) (j : re −1 i ) }× (T + : FunOrn T )
FunOrn
1
∋ 1

18

From a functional ornament, we get the type of the liftings by interpreting the ornaments
as we go along:
J(T + : FunOrn T )KFunOrn
Jµ+{O (inv j ) }→ T + KFunOrn
Jµ+{O (inv j ) }× T + KFunOrn
J1KFunOrn

:
7
→
7
→
7
→

Set
µ JO Korn j → JT + KFunOrn
µ JO Korn j × JT + KFunOrn
1

We will want our ornamented function to be coherent with the base function we started
with: for a function f : µ D → µ E, the ornamented function f + : µ JOD Korn → µ JOE Korn
is said to be coherent with f if the following diagram commutes:
µ JOD Korn

f+

OD -forget
µD

µ JOE Korn
OE -forget

f

µE

Or, equivalently in type theory:
∀x + : µ JOD Korn .f (OD -forget x + ) ≡ OE -forget (f + x + )
To generalise the definition of coherence to any arity, we generically define it by induction
over the universe of functional ornaments:
Coherence(T + : FunOrn T )(f : JT KType )(f + : JT + KFunOrn ) : Set
Coherence (µ+{O (inv j ) }→ T + ) f
f+
7→
+
+
+
∀x : µ JOKorn j .Coherence T (f (forgetOrn x )) (f + x + )
Coherence (µ+{O (inv j ) }× T + ) (x , xs) (x + , xs + )
7→
+
+
+
x ≡ forgetOrn x × Coherence T xs xs
Coherence
1
∗
∗
7→
1
Example 3 (Ornamenting type< to describe lookup). In Section 2, we have identified
the ornaments involved to transport the type of < to obtain the type of lookup. Let
us spell them in full here. We need to ornament Nat into ListA and Bool into MaybeA :
data List [A : Set] from Nat where
ListA ∋ nil
| cons [a : A](as : ListA )
data Maybe [A : Set] from Bool where
MaybeA ∋ just [a : A]
| nothing

19

From there, we give the functional ornament describing the type of the lookup function:
typeLookup : FunOrn type<
typeLookup 7→ µ+{idONat ∗ }→ µ+{List-Orn ∗ }→ µ+{Maybe-Orn ∗ }× 1
The user can verify that JtypeLookupKFunOrn gives us the type of the lookup function, up
to multiplication by 1. Also, computing Coherence typeLookup ( < ) gives the expected
result:
λf + : JtypeLookupKFunOrn .
∀n : Nat.∀xs : ListA .isJust (f + n xs) ≡ n < length xs
Note that 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.
Example 4 (Ornamenting type+ to describe ++ ). The functional ornament of type+
makes only use of the ornamentation of Nat into ListA :
type++ : FunOrn type+
type++ 7→ µ+{List-Orn ∗ }→ µ+{List-Orn ∗ }→ µ+{List-Orn ∗ }× 1
Again, computing Jtype++KFunOrn indeed gives us the type of ++ while Coherence type++( + )
correctly captures our requirement that list append preserves the length of its arguments.
As before, the list append function is not the only valid lifting: one could for example
consider a function that reverts the first list and appends it to the second one.

4.3 Patches
By definition of a functional ornament, the lifting of a base function f : JT KType is a
function f + of type JT + KFunOrn satisfying the coherence property Coherence T + f . To
implement a lifting that is coherent, we might ask the user to first implement the lifting
f + and then prove it coherent. 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.
Note that we are looking for an equivalence here: we will define patches so that they
are in bijection with liftings satisfying a coherence property, informally:
Patch T T + f ∼
= (f + : JT + KFunOrn ) × Coherence T + f f +

(1)

In this paper, we constructively use this bijection in the left to right direction: having
implemented a patch f ++ of type Patch T T + f , we will show, in the next Section, how
we can extract a lifting together with its coherence proof.
Before giving the general construction of a Patch, let us first work through the < example. After having functionally ornamented < with typeLookup, the lifting function

20

f + and coherence property can be represented by the following commuting diagram:
Nat
id
Nat

×

ListA

f+

List-forget
×

MaybeA
Maybe-forget

Nat

<

Bool
(2)

In type theory, this is written as:
(f + : Nat × ListA → MaybeA ) ×
∀m : Nat.∀as : ListA .m < List-forget as ≡ Maybe-forget (f + m as)
Applying dependent choice, this is equivalent to:
∼
= (m : Nat) × (n : Nat) × (as : ListA ) × List-forget as ≡ n →
(ma : MaybeA ) × Maybe-forget ma ≡ m < n
Now, by definition of reornaments, we have that:
(as : ListA ) × List-forget as ≡ n ∼
= VecA n
(ma : MaybeA ) × Maybe-forget ma ≡ b ∼
= IMaybeA b

and

Applying these isomorphisms, we obtain the following type, which we call the Patch of
the functional ornament typeLookup:
∼
= (m : Nat) × (n : Nat) × (vs : VecA n) → IMaybeA (m < n)
Which is therefore equivalent to a pair of a lifting and its coherence proof.
Intuitively, the Patch construction consists in turning all the vertical arrows of the
commuting diagram (2) into the equivalent reornaments, or put in type theory: turning
the pairs of data and their algebraically defined constraint into equivalent reornaments.
The coherence property of reornaments tells us that projecting the ornamented function
down to its unornamented 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 (here, introducing m and n)
and index the return types by the result of the unornamented function (here, indexing
IMaybeA by the result m < n).
It is easy to generalise this construction to any functional ornament. For clarity, we
shall only write the proof for arity one. The generalisation to multiple input and output
arities is straightforward but tediously verbose. So, from a base function f , we start
with its lifting and the associated coherence property:
(f + : µ JOA Korn → µ JOB Korn ) ×
∀a + : µ JOA Korn .OB -forget(f + a + ) ≡ f (OA -forget a + )

21

Applying dependent choice, we obtain the following equivalent type:
∼
= (a : µ A) × (a + : µ JOA Korn ) × OA -forget a + ≡ a → (b + : µ JOB Korn ) × OB -forgetb + ≡ f a
Then, we can simply use the characterisation of a reornament to turn every pair (x + :
µ JOX Korn ) × OX -forget x + ≡ t into the equivalent inductive type µ X OX t:
∼
= (a : µ A) × µ AOA a → µ B OB (f a)
To build this type generically, we simply proceed by induction over the functional
ornament. Upon an argument (i.e. a µ+{O }→ ), we introduce a fresh index and the
reornament of O. Upon a result (i.e. a µ+{O }× ), we ask for a reornament of O indexed
by the result of the base function.
Patch
(T : Type)
(T + : FunOrn T ) (f : JT KType )
+
Patch (µ{D (re j ) }→ T ) (µ {O (inv j ) }→ T + )
f
(x : µ D (re j )) → µ D O (j , x ) → Patch T T + (f x )
Patch (µ{D (re j ) }× T ) (µ+{O (inv j ) }× T + ) (x , xs)
µ D O (j , x ) × Patch T T + xs
Patch
1
1
∗

: Set
7→
7→
7→ 1

Example 5 (Patch of typeLookup). The type of the coherent liftings of < by typeLookup,
as defined by the Patch of < by typeLookup, computes to:
(m : Nat)(m + : µ NatidONat m) → (n : Nat)(vs : µ NatListA n) → µ BoolMaybeA (m < n) × 1
Note that µ NatidONat n 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. Hence, we discard this argument as computationally uninteresting.
On the other hand, NatListA and BoolMaybeA are, respectively, the previously introduced
VecA and IMaybeA types.
Example 6 (Patch of type+). Similarly, the Patch of + by type+ computes to:
(m : Nat)(xs : NatListA m) → (n : Nat)(ys : NatListA m) → NatListA (m + n) × 1
Which is the type of the vector append function.

4.4 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.

22

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 isomorphism (1)
of the previous Section through our constructive glasses: indeed, as the Patch type is
isomorphic to the set of liftings satisfying the coherence property, we effectively get a
function taking every Patch to a lifting and its coherence proof. More precisely, we
obtain the lifting by generalising the reornament-induced ∗-forget maps to functional
ornaments while we obtain the coherence proof by generalising the reornament-induced
coherentOrn theorem to functional ornaments.
We call patching the action of projecting the coherent lifting from a Patch function.
Again, it is defined by mere induction over the functional ornament. When ornamented
arguments are introduced (i.e. with µ+{O }→ ), we simply patch the body of the function.
This is possible because from x+ : µ JOD Korn , we can forget the ornament to compute
f (forgetOrn x+ ) and we can also make the reornament to compute f ++ (makeAlgOrn x+ ).
When an ornamented result is to be returned, we simply forget the reornamentation
computed by the coherent lifting:
patch (T + : FunOrn T ) (f : JT KType ) (p : Patch T T + f )
f
f ++
patch (µ+{O (inv j ) }→ T + )
λx + . patch (f (forgetOrn x + ))
(f ++ (forgetOrn x + ) (makeAlgOrn x + ))
patch (µ+{O (inv j ) }× T + ) (x , xs)
(x ++ , xs ++ )
++
+
++
(forgetOrn x , patch T xs xs )
patch
1
∗
∗

: JT + KFunOrn
7
→

7→
7→ ∗

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: this is a straightforward application of
the coherentOrn theorem:
coherence (T + : FunOrn T ) (f : JT KType ) (p : Patch T T + f )
coherence (µ+{O (inv j ) }→ T + )
f
p
λx + . coherence T +
(f (forgetOrn x + ))
(p (forgetOrn x + ) (makeAlgOrn x + ))
+
coherence (µ {O (inv j ) }× T + ) (x , xs)
(x + , p)
(coherentOrn x + , coherence T + xs p)
coherence
1
∗
∗

: Coherence T + f (patch T + f p)
7
→

7→
7→ ∗

Example 7 (Obtaining lookup and its coherence certificate, for free). This last step is
a mere application of the patch and coherence functions. Hence, we define lookup as
follows:
lookup : JtypeLookupKFunOrn
lookup 7→ patch typeLookup ( < ) ilookup

23

And we get its coherence proof, here spelled in full:
cohLookup (n : Nat) (xs : ListA ) : Maybe-forget (π0 (lookup n xs)) ≡ π0 (n < List-forget xs)
cohLookup
n
xs
7→ coherence typeLookup ( < ) ilookup n xs
Example 8 (Obtaining ++ and its coherence certificate, for free). Assuming that we
have implemented the coherent lifting vappend, we obtain concatenation of lists and its
coherence proof by simply running our generic machinery:
++ : Jtype++KFunOrn
++ 7→ patch type++ ( + ) vappend
coh++ (xs : ListA ) (ys : ListA ) : List-forget (π0 (xs ++ ys)) ≡ π0 ((List-forget xs) +(List-forget ys))
coh++
xs
ys
7→ coherence type++ ( + ) vappend xs ys

Looking back at the manual construction in Section 2, we can measure the progress
we have made: while we had to duplicate entirely the type signature of lookup and its
coherence proof, we can now write down a functional ornament and these are generated
for us. This is not just convenient: by giving a functional ornament, we establish a
strong connection between two functions. By pinning down this connection with the
universe of functional ornaments, we turn this knowledge into an effective object that
can be manipulated and reasoned about within the type theory.
We make use of this concrete object 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 as the type of the liftings coherent by construction. As we have
seen, its construction and further projection down to a lifting is now 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. We have now
made this second alternative just as accessible as the first one. And, from a programming
perspective, the second approach is much more appealing. In a word, we have made an
appealing technique extremely cheap!
Finally, we shall reiterate that none of the above constructions involve extending the
type theory: for a theory with a universe of datatypes, the theory of functional ornaments
can be entirely internalised as a few generic programs and inductive types. For a system
lacking a universe of datatypes, this technology would need to be provided at the metalevel. However, the fact that our constructions type-check in our system suggests that
adding these constructions at the meta-level is consistent with a pre-existing meta-theory.

24

m

<
< n
m
< 0
m
< suc n
0
< suc n
suc m < suc n

:
⇐
7
→
⇐
7
→
7
→

Jtype<KType
Nat-case n
(false, ∗)
Nat-elim m
(true, ∗)
m <n

ilookup
(m : Nat) (vs : VecA n)
ilookup
m
vs
ilookup
m
nil
ilookup
m
(cons a vs)
ilookup
0
(cons a vs)
ilookup (suc m) (cons a vs)

:
⇐
7
→
⇐
7
→
7
→

IMaybeA (m < n)
Vector-case vs
nothing
Nat-elim m
just a
ilookup m vs

Figure 4: Implementations of < and ilookup

5 Lazy programmers, clever 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. 4). First, both functions follow the
same recursion pattern: case analysis over n/vs followed by induction 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 will be used in ilookup. Interestingly, the only unknown, hence the only necessary
input from the user, is the a in the just case: it 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 duplicate and only provides strictly necessary inputs. We are
primarily interested in transporting two forms of structure:
Recursion pattern: if the base function is a fold LαM and the user provides us with a
coherent algebra β̂ of α, we automatically construct the coherent lifting Lβ̂M of LαM
;
Returned constructor: if the base function returns a constructor C and the user provides
us with a coherent extension Ĉ of C, we automatically 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, automatically and
generically, build the lifted folds and values.

5.1 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 transportation is that the
lifting uses exactly the same structure to compute its results. Hence, in the majority
of the cases, we could just ask the computer to use the induction principle induced by

25

the base one: the only task left to the user will be to give the algebra. For clarity
of exposition, we restrict ourselves to transporting folds. However, the treatment of
induction is essentially the same, as hinted by the fact that induction can be reduced to
folds [Fumex et al., 2011].
To understand how we transport the recursion pattern, let us look again at the coherence property of liftings, but this time specialising to functions that are folds:
µ JOD Korn

LβM

JT + KFunOrn
T + -forget

OD -forget
µD

JT KType

LαM

By the fold-fusion theorem [Bird and de Moor, 1997], it is sufficient (but not necessary)
to work on the algebras, where we have the following diagram:
β

JJOD Korn K JT + KFunOrn
JOD K T + -forget
JJOD Korn K JT KType

OD -forgetNat

JT + KFunOrn
T + -forget

JDK JT KType

α

JT KType

Now, we would like to find an algebra β̂ such that its fold gives us a function of the
Patch type.
To illustrate this approach, we work through a concrete example: we derive hd :
ListA → MaybeA from isSuc : Nat → Bool by transporting the algebra. For the sake of
argument, we artificially define isSuc by a fold:
isSuc (n : Nat) : Bool
isSuc
n
7→ LαisSuc M n where
αisSuc (xs : JNat-DescK Bool) : Bool
αisSuc
’0
7→ false
αisSuc
(’suc xs)
7→ true
Our objective is thus to define the algebra for hd, which has the following type:
αhd : JList-DescK MaybeA → MaybeA
such that its fold is coherent. By the fold-fusion theorem [Bird and de Moor, 1997], it
is sufficient (but not necessary) for αhd to satisfy the following condition:
∀ms : JList-DescK MaybeA .
isJust (αhd ms) ≡ αisSuc (List-forgetNat(JList-DescK isJust ms))

26

Following the same methodology we applied to define the Patch type, we can massage
the type of αhd and its coherence condition to obtain an equivalent definition enforcing
the coherence by indexing. In this case, the natural candidate is:
αihd : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n → IMaybeA (isSuc n)
This construction generalises to any functional ornament. That is, from an algebra
α : (i : I) → JD i K (λ . JT KType ) → JT KType
together with an ornament OD : orn re D and a functional ornament T + : FunOrn T , the
type of coherent algebras for α is:
β̂ : (j : J)(t : µ D (re j )) →
JD O (j , t)K (λ(j , t ). Patch T (LαM t) T + ) →
Patch T (LαM t) T +
It can formally be proved that algebras of this type capture exactly the algebras satisfying the coherence condition. Constructively, we get that such a coherent algebra induces
a coherent lifting, by a mere fold of the coherent algebra:
lift-fold (α : (i : I ) → JD i K (λ . JT KType ) → JT KType )
(β̂ : (j : J )(t : µ D (re j )) →
JD O (j , t )K (λ(j , t). Patch T (LαM t) T + ) →
Patch T (LαM t) T + )
: Patch (µ{D (re j ) }→ T ) LαM (µ+{O j }→ T + )
lift-fold α β̂ 7→ λx . λx ++ . Lβ̂M x ++
Generalising this idea, we similarly lift induction:
lift-ind (α : (i : I )(xs : JD i K µ D) →
iAll D (λ . JT KType ) xs → JT KType )
(β̂ :(j : J )(t : µ D (re j ))(xs : JD O (j , t)K µ D O ) →
iAll (D O (λ(j , t). Patch T ((iinduction α) t) T + ) xs →
Patch T ((iinduction α) t) T + )
: Patch (µ{D (re j ) }→ T ) (iinduction α) (µ+{O j }→ T + )
lift-ind α β̂ 7→ λx . λx ++ . iinduction β̂ x ++
Lifting case analysis is now simple, as case analysis is a specialisation of induction
where the induction hypotheses are stripped out [McBride et al., 2004]:

27

lift-case (α : (i : I)(xs : JD i K µ D) → JT KType )
(β̂ : (j : J )(t : µ D (re j ))
(xs : JD O (j , t )K µ D O ) →
Patch T ((iinduction (λxs . α xs)) t) T + )
: Patch (µ{D (re j ) }→ T )
(iinduction (λxs . α xs))
(µ+{O j }→ T + )
lift-case α β̂ 7→ lift-ind (λxs . α xs) (λxs . β̂ xs)
Example 9 (Transporting the recursion pattern of isSuc). We can now apply our generic
machinery to transport isSuc to hd: in a high-level notation, we would write the command
of Fig. 5(a). To this command, an interactive system would respond by automatically
generating the algebra, as shown in Fig. 5(b). In the low-level type theory, this would
elaborate to the following term:
ihd (vs : VecA n) : IMaybeA (isSuc n)
ihd
vs
7→ lift-fold αisSuc αihd where
αihd (vs : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n) :
IMaybeA (isSuc n)
αihd
’nil
7→ {?}
αihd
(’cons a xs)
7→ {?}
Once again, it is beyond the scope of this paper to formalise the elaboration process from
the high-level notation to the low-level type theory. The reader will convince himself that
the high-level notation contains all the information necessary to conduct this task. We
shall now freely use the high-level syntax, with the understanding that it automatically
builds a type theoretic term that type-checks.
Example 10 (Transporting the recursion pattern of < ). To implement ilookup, we
use lift-case to transport the case analysis on n and lift-ind to transport the induction
over m. In a high-level notation, this interaction results in:
ilookup : Patch type< typeLookup <
ilookup
ilookup

m
m

mm
mm

n
0

vs
nil

lift

⇐ lift-case
{?}
lift

ilookup
m
m m (suc n) (cons a vs) ⇐ lift-ind
ilookup
0
0
0
nil
{?}
ilookup (suc m) (suc m m ) 0
nil
{?}
It is crucial to understand here that, in an interactive setting, the user would type in
lift
the ⇐ command together with the action to be carried out and the computer would
automatically generate the resulting patterns.

28

Example 11 (Transporting the recursion pattern of + ). In order to implement
vappend, 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 we
are left filling the following goals:
vappend : Patch type+ type++ +
vappend
m
xs
n ys
0
nil
n ys
vappend
vappend (suc m) (cons a xs) n ys

lift

⇐ lift-case
{?}
{?}

5.2 Transporting constructors
Just as the recursive structure, the returned values often simply mirror the original
definition: we are 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 the constructor, the computer should fill in the parts that are already
determined by the original constructor and ask only for the missing information, i.e. the
data freshly introduced by the ornament.
Remember that, when implementing the coherent lifting, we are working on the reornaments of the lifting type. Hence, when returning a constructor-headed value, we are
building an inhabitant of a reornament. When defining reornaments in Section 3.2.2,
we have shown that, thanks to deletion ornaments, a reornament can be decomposed in
two components:
• first, the extension that contains all the extra information introduced by the ornament ;
• second, the recursive structure of the refined datatype, which defines the type of
the arguments of the constructor
And no additional information is required: all the information provided by indexing with
the unornamented datatype is optimally used in the definition of the reornament. There
is absolutely no duplication of information.
This clear separation of concern is a blessing for us: when lifting a constructor, we
only have to provide the extension and the arguments of the datatype, nothing more.
In term of implementation, this is as simple as:
lift-constructor (xs : JD (re j )K µ D )
– coherent extension
(e : Extension (O j ) xs)
(a : JJStructure O xs eKorn K (µ D O )) – arguments
(t ++ : Patch T t T + )
: Patch (µ{D (re j ) }× T )
(in xs, t)
(µ+{O j }× T + )
++
lift-constructor xs e a t
7→ (in (e, a), t ++ )

29

Example 12 (Transporting the constructors of isSuc). 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. 5(c). The interactive system would then respond by generating the code of
Fig. 5(d). The 1 goals are trivially solved, probably automatically by the system. The
only information the user has to provide is a value of type A returned by the just
constructor.
Example 13 (Transporting the constructors of < ). In the implementation of ilookup,
we want to lift the returned true and false to the Maybe ornament. In a high-level
notation, this would be represented as follows:
:

ilookup

Patch type< typeLookup <

lift

m

mm

n

vs

⇐ lift-case

ilookup

m

mm

0

nil

7→ nothing ∗[∗]

ilookup

m

mm

ilookup

lift

lift

(suc n) (cons a vs) ⇐ lift-ind
lift

ilookup
0
0
(suc n) (cons a vs) 7→ just {? : a} A[∗]
ilookup (suc m) (suc m m ) (suc n) (cons a vs) {?}
As before, in an interactive setting, the user would instruct the machine to execute the
lift
command 7→ and the computer would come back with the skeleton of the expected
inputs. Finishing the implementation of ilookup is now one baby step away, which we
should jump straightaway:
: Patch type< typeLookup <

ilookup

lift

m

mm

n

vs

⇐ lift-case

ilookup

m

mm

0

nil

7→ nothing ∗[∗]

ilookup

m

mm

ilookup

lift

lift

(suc n) (cons a vs) ⇐ lift-ind
lift

ilookup
0
0
(suc n) (cons a vs) 7→ just a[∗]
ilookup (suc m) (suc m m ) (suc n) (cons a vs) →
7 ilookup m m m n vs

Example 14 ([Transporting the constructors of + ). 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 and get the following goals as a
result:
vappend : Patch type+ type++ +
lift

n
n

ys
ys

⇐ lift-case
{?}

vappend (suc m) (cons a xs) n

ys

7→ cons {? : A} [ {?} ]

vappend
vappend

m
0

xs
nil

lift

It is then straightforward to, manually this time, conclude the implementation of

30

vappend:
vappend : Patch type+ type++ +
lift

n
n

ys
ys

⇐ lift-case
7 ys
→

vappend (suc m) (cons a xs) n

ys

7→ cons a[vappend m xs n ys]

vappend
vappend

m
0

xs
nil

lift

6 Removing index-level computations
For a seasoned programmer, the type of ilookup might appear rather unconventional:
ilookup : (m : Nat)(vs : VecA n) → IMaybeA (m < n)
Indeed, lookup in a vector is traditionally given the following type:
vlookup : (m : Fin n)(vs : VecA n) → A
The issue with the first presentation is that the return type is indexed by a computed
value, m < n. This means that, provided that we have an x : IMaybeA k and we want to
return it, we must first make sure that the computation of m < n has unfolded to k, where
k might be a value (such as true or false) or a suspended computation (such as suc m < n).
Making sure that this index-level computation unfolds correctly can be cumbersome at
best, and sometimes simply impossible. One then has to manually rewrite the goal using
proofs. Again, this pollutes the function definition with computationally unnecessary
details.
On the other hand, the second presentation requires absolutely no special care to
indexes, nor any need for proofs. The key difference is in handling the constraint that
m must be less than the length of the vector. In the first case, we make no assumption
on m as an input and then constrain the result to be meaningful if m < n and pointless
otherwise (by definition of IMaybe). In the second case, we restrict the input m to be
less than n (by stating that m : Fin n) and therefore the result is always meaningful.

6.1 From ilookup to vlookup, manually
It is intuitively clear that these two presentations are equivalent. However, sometimes
it is easier to work with the first (e.g. because we use our lifting machinery that, by
design, unfolds the indexed computation as wanted) or with the second (e.g. the recursion
pattern we want does not mirror the one of the indexed computation). Let us look closer
at this equivalence, factoring out the vector that has no influence here:
(m : Nat) → IMaybeA (m < n) ∼
= Fin n → A
While this seems to suggest an adjunction, it is not clear what the functors are. Rewriting
the equation more abstractly help to see clearer:
·
1 Nat → IMaybeA ( < n) ∼
= Fin n → A

31

·

Where 1 is the map from Nat to 1 and P → Q is defined as (x : Nat) → P x → Q x .
Having done that, we can make a more informed guess on the right adjoint: it is the
functor λX : Nat → Set. λm : Nat. X ◦ ( < n).
Now, as for the left adjoint, we must extract a functor that would map 1 Nat to Fin n.
The semantics of Fin n is of great help here: intuitively, an inhabitant of Fin n is a number
m : Nat such that m < n, or put otherwise
Fin n ∼
= {m ∈ Nat | m < n}
As we have seen in Section 3.2.1, these two presentations are equivalent: seen as the algebraic ornament by the algebra of < n, Fin n can be decomposed as a number (as computed by Natα< -forget) and a proof (as computed by coherentOrn). Following Atkey et al.
[2011], we translate this into category, obtaining that Fin n ∼
= Σ( < n) ◦ 1 Nat. This suggests the following equivalences:
·
1 Nat → IMaybeA ( < n) ∼
= Fin n → A
·
∼
= Σ( < n) 1 Nat → IMaybeA

The second and third line are indeed equivalent: the third line maps predicates over Bool,
which might seem as more general than the second line, however in the false, IMaybe
simplifies to 1. Hence, the only interesting case happens when the index is true, in which
case IMaybe simplifies to .
With this more abstract presentation, it should be clear what the left adjoint must
be: it is Σ( < n) . Now we have to check that Σ( < n) is indeed left adjoint to ◦ ( < n): it
is actually true in any locally cartesian closed-category (LCCC). Hence, a fortiori, this
is true in type theory, as type-theories are a model of LCCCs.

6.2 Reindexing and algebraic ornaments
In all generality, we prove the following equivalence:
(m : µ D) → µ E (LαM m) ∼
= µ Dα n → µ E n
The proof is straightforward, following the intuition we gave above:
·
(m : µ D) → µ E (LαM m) ∼
= 1µ D → µ E ◦ LαM
·
∼
= ΣLαM 1µ D → µ E
·
∼
= µ JD α Korn → µ E

(abstract the index)
(Σf ⊣ ◦ f )
(coherence of algebraic ornament)

Through our constructive glasses, this categorical equivalence correspond to two rather
interesting functions: in one direction, rlAdjoint transforms a function with index-level
computation into one with a stronger premise ; in the other direction, lrAdjoint turns a
function with strong premises into one with index-level computation. The implementation is absolutely unsurprising: we translate the categorical proof into its corresponding

32

constructive operation, i.e. the coherentOrn theorem and the -make function:
rlAdjoint (f : (i : I )(t : µ D i ) → µ E (i , LαM t))
(i : I )(x : X i )(t x : µ JD α Korn (i , x )) : µ E (i , x )
rlAdjoint f i x t x 7→ subst (λx . µ E (i , x )) (sym (coherentOrn i x t x )) (f (D α -forget t x ))
lrAdjoint (g : (i : I )(x : X i )(t x : µ JD α Korn (i , x )) → µ E (i , x ))
(i : I )(t : µ D i ) : µ E (i , LαM t)
lrAdjoint g i t 7→ g (D α -make t)
We should finally add that this construction is in no sense restricted to the functions
computed by Patch: the relation we have established and made concrete here can be used
for any function. Of general interest is the function lrAdjoint: instead of tediously unfolding the computation LαM, the programmer can instead build the alternative function
without having to care about the recursion pattern introduced by α.
In our framework, the rlAdjoint is more interesting: our clever constructors make it
easy to unfold the index-level computation, however, in practice, one will rather use the
equivalent function using richer data-types. Hence, our user can implement the Patch
using our machinery while still getting the more convenient function.
Example: from ilookup to vlookup. Using the gadget we have just developed, we can
now obtain vlookup automatically from the definition of ilookup:
vlookup (m : Fin n) (vs : VecA n) : A
vlookup
m
vs
7→ rlAdjoint (λm. ilookup m vs)∗ true m

7 Related work
Our work is an extension of the work of McBride 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, therefore, deletion of duplicated information was impossible. A
corollary of this was that reornaments contained a lot of duplication, hence making the
lifting of value from ornamented to reornamented datatype extremely tedious.
Our presentation of algebraic ornament has been greatly improved by the categorical
model developed by Atkey et al. [2011]: 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.

33

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 folds
is a trivial specialisation of induction. Also, the characterisation of the fix-point of an
algebraic ornament as op-reindexing of the fold is a key ingredient to understanding
index-level computations and assimilate them at the term level.
In their work on realisability and parametricity for Pure Type Systems, Bernardy and
Lasson [Bernardy and Lasson, 2011] 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 contribution and their 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 realisability predicate. The strength of
the realisability interpretation is that it is naturally defined on functions: while McBride
and Atkey et al. [2011] only consider ornaments on datatypes, their work is the first, to
our knowledge, to capture a general notion of functions realising – i.e. ornamenting –
other functions.
Following the steps of Bernardy, Ko and Gibbons [2011] adapted the realisability interpretation to McBride’s universe of datatypes and explored the other direction of the
Patch equivalence, 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 equivalence 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 functions 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 realisability
predicate constructions of Bernardy and Lasson [2011], Ko and Gibbons [2011].

8 Conclusion
In this paper, we have developed the notion of functional ornament and shown how one
can achieve code reuse by transporting functions along a functional ornament. To this
end, we have adapted McBride’s ornaments to our universe of datatypes [Chapman et al.,
2010]. This gave us the ability to compute over indices, hence introducing the deletion
ornament. Deletion ornaments are a key ingredient to the internalisation of Brady’s
optimisation [Brady et al., 2004] over inductive families. In particular, this gave us a
simpler implementation of reornaments.
We then generalised ornaments to functions: from a universe of function type, we
define a functional ornament as the ornamentation of each of its inductive components.

34

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.
Having functional ornaments, this raises the question of transporting a function to its
ornamented version in such way that the coherence property holds. Instead of asking our
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 offered by the environment: 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 get, for free, the lifting and its coherence certificate. This is a straightforward application of the equivalence
between 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 two clever 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 element 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 able to organise
datatypes by their structure. With functional ornaments, we are now able to organise
functions by their structure-preserving computational behaviour. Besides, we have developed some appealing automation to assist the implementation of functional ornaments,
without any proving required, hence making this approach even more accessible.

8.1 Future work
Whilst we have deliberately chosen a simple universe of functions, we plan to extend it
in various directions. Adding type dependency (Π- and Σ-types) but also non inductive
sets is a necessary first step. Inspired by Bernardy [2011] but also Miquel [2001], we
would like to add a parametric quantifier: in the implementation of ilookup, we would
like to mark the index A of VecA and IMaybeA as parametric so that in the cons a case,
the a could automatically be carried over to just a.
The universe of functional ornaments could be extended as well, especially once the
universe of functions 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 fixed points in this paper, we also
want to generalise our universe with greatest fixed points and the lifting of co-inductive
definitions.
Further, our framework relies crucially on the duality between a reornament and its
ornament presentation subject to a proof. We cross this isomorphism in both directions

35

when we project the lifting from the coherent lifting. In practice, this involves a traversal
of each of the input datatypes and a traversal of each of the output datatypes. However,
computationally, these traversal are identities: the only purpose of these terms is at the
logical level, for the type-checker to fix the types. We are looking at transforming our
library of clever constructor into a proper domain-specific language (DSL). This way,
implementing a coherent lifting would consists in working in a DSL. Projecting the lifting
and its coherence proof would then be the work of an optimising compiler that would
compute away the useless translations.
Finally, much work remains to be done on the front of usability: for convenience, we
have presented some informal notations for datatypes, their ornaments and an extension
of Epigram programming facility with liftings. A formal treatment of these syntaxes and
of their elaboration to the low-level type theory is underway.
Acknowledgements We owe many thanks to our colleagues in the MSP group for many
fruitful discussions. We are in particular grateful to Guillaume Allais, Stevan Andjelkovic
and Peter Hancock for their meticulous reviews of several drafts of this paper. We shall
also thank Edwin Brady for suggesting the family of lookup functions as a prolific source
of functional ornaments 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 José Pedro Magalhães.

References
R. Atkey, P. Johann, and N. Ghani. When is a type refinement an inductive type? In
Proceedings of the 14th international conference on Foundations of software science
and computational structures, pages 72–87, Berlin, Heidelberg, 2011. Springer-Verlag.
J.-P. Bernardy. A Theory of Parametric Polymorphism and an Application. PhD thesis,
Chalmers University of Technology, 2011.
J.-P. Bernardy and M. Lasson. Realizability and parametricity in pure type systems. In
M. Hofmann, editor, FOSSACS, volume 6604 of Lecture Notes in Computer Science,
pages 108–122. Springer, 2011. ISBN 978-3-642-19804-5.
R. S. Bird and O. de Moor. Algebra of programming. Prentice Hall International series
in computer science. Prentice Hall, 1997. ISBN 978-0-13-507245-5.
E. Brady, C. McBride, and J. McKinna. Inductive families need not store their indices.
In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs,
volume 3085 of Lecture Notes in Computer Science, pages 115–129. Springer Berlin /
Heidelberg, 2004.
J. Chapman, P.-E. Dagand, C. McBride, and P. Morris. The gentle art of levitation.
SIGPLAN Not., 45:3–14, September 2010.

36

J. Cheney and R. Hinze. First-class phantom types. Technical report, Cornell University,
2003.
T. Coquand. Pattern matching with dependent types. In B. Nordström, K. Petersson,
and G. Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and
Programs, 1992.
P. Dybjer. Inductive families. Formal Asp. Comput., 6(4):440–465, 1994.
T. Freeman and F. Pfenning. Refinement types for ML. SIGPLAN Not., 26:268–277,
May 1991.
C. Fumex, N. Ghani, and P. Johann. Indexed induction and coinduction, fibrationally.
In A. Corradini, B. Klin, and C. Cı̂rstea, editors, CALCO, volume 6859 of Lecture
Notes in Computer Science, pages 176–191. Springer, 2011.
C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting.
Inf. Comput., 145(2):107–152, 1998.
H.-S. Ko and J. Gibbons. Modularising inductive families. In J. Jrvi and S.-C. Mu,
editors, Workshop on Generic Programming, pages 13–24, 2011.
C. McBride. Ornamental algebras, algebraic ornaments. Journal of Functional Programming, to appear.
C. McBride and J. McKinna. The view from the left. J. Funct. Program., 14(1):69–111,
2004.
C. McBride, H. Goguen, and J. McKinna. A few constructions on constructors. In J.-C.
Filliâtre, C. Paulin-Mohring, and B. Werner, editors, TYPES, volume 3839 of Lecture
Notes in Computer Science, pages 186–200. Springer, 2004.
A. Miquel. The implicit calculus of constructions. In TLCA, pages 344–359, 2001.
P. Morris, T. Altenkirch, and N. Ghani. A universe of strictly positive families. Int. J.
Found. Comput. Sci., 20(1):83–107, 2009.
U. Norell. Towards a practical programming language based on dependent type theory.
PhD thesis, Chalmers University of Technology, 2007.
N. Swamy, J. Chen, C. Fournet, P.-Y. Strub, K. Bhargavan, and J. Yang. Secure distributed programming with value-dependent types. In ICFP, pages 266–278, New
York, NY, USA, 2011. ACM. ISBN 978-1-4503-0865-6.
The Coq Development Team. The Coq Proof Assistant Reference Manual.
H. Xi, C. Chen, and G. Chen. Guarded recursive datatype constructors. In POPL, 2003.

37

(a) Request lifting of algebra (user input):
ihd (vs : VecA n) : IMaybeA isSuc n
lift

⇐ lift-fold

ihd
{?}

(b) Result of lifting the algebra (system output):
ihd (vs : VecA n) : IMaybeA (isSuc n)
ihd

lift

⇐ lift-fold where
αihd (vs : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n) : IMaybeA (isSuc n)
αihd
’nil
{?}
αihd
(’cons a xs)
{?}

(c) Request lifting of constructors (user input):
ihd (vs : VecA n) : IMaybeA (isSuc n)
ihd

lift

⇐ lift-fold where
αihd (vs : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n) : IMaybeA (isSuc n)
lift

αihd

’nil

7→ {?}

αihd

(’cons a xs)

7→ {?}

lift

(d) Result of lifting constructors (system output)
ihd (vs : VecA n) : IMaybeA (isSuc n)
ihd

lift

⇐ lift-fold where
αihd (vs : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n) : IMaybeA (isSuc n)
αihd

’nil

αihd

(’cons a xs)

lift

7→ nothing {? : 1} [ {? : 1} ]
lift

7→ just {? : A} [ {? : 1} ]

(e) Type-checked term (automatically generated from (d)):
ihd (vs : VecA n) : IMaybeA (isSuc n)
ihd
vs
7→ lift-fold αisSuc αihd where
αihd (vs : JVec-DescK (λn ′ . IMaybeA (isSuc n ′ )) n) : IMaybeA (isSuc n)
αihd
’nil
7→ lift-constructor ’nil {? : 1} {? : 1} ∗
αihd
(’cons a xs)
7→ lift-constructor (’suc n) {? : A} {? : 1} ∗

Figure 5: Guided implementation of ihd

38

