https://personal.cis.strath.ac.uk/conor.mcbride/pub/OAAO/Ornament.pdf, http://mazzo.li/epilogue/index.html%3Fp=577.html, http://morphis.me/link/ornaments-practice.pdf

Ornaments.agda

-- Ornaments explore the transformation of "simple" datatypes by introducing
-- an indexing structure that allows decorating the type with extra information.
module Ornaments where

open import Agda.Primitive

record ⊤ : Set where
  constructor ⋆

data _≡_ ..{ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
  refl : x ≡ x
{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

infixr 2 _×_
infixr 4 _,_

record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  constructor _,_
  field
    fst : A
    snd : B fst
open Σ public

_×_ : ∀ {a b} (A : Set a) (B : Set b) → Set (a ⊔ b)
A × B = Σ A (λ x → B)

-- Tagged naturals
data NatT : Set where
  zz ss : NatT

-- Plain, unindexed, first-order data structures.
-- "You can interpret a Plain description as a format, or a program for reading
-- a record corresponding to one node of the tree."
data PlainDesc : Set₁ where
  -- Read field in A; continue with its value
  arg : (A : Set) → (A -> PlainDesc) → PlainDesc
  -- Read a recursive subnode; continue regardless
  rec : PlainDesc → PlainDesc
  -- Stop reading.
  ret : PlainDesc

-- Describes the structure of the natural numbers [with tags].
NatPlain : PlainDesc
NatPlain = arg NatT λ { zz → ret -- If zero, we're done here.
                      ; ss -> rec ret -- Otherwise we have a subnode that yields a predecessor.
                      }

-- Desugar into Agda-isms.
⟦_⟧P : PlainDesc → Set → Set
⟦ (arg A D) ⟧P R = Σ A (λ a → ⟦ D a ⟧P R) -- I am become Reader Monad
⟦ (rec D) ⟧P R = R × ⟦ D ⟧P R -- Continue and build a product
⟦ ret ⟧P R = ⊤ -- Halt at the top

-- The fixpoint of a Plain Description is Plain Data.
data PlainData (D : PlainDesc) : Set where
  ⟨_⟩ : ⟦ D ⟧P (PlainData D) → PlainData D

-- The naturals in Plain Data
NatPD : Set
NatPD = PlainData NatPlain

-- Earlier we said zero had a subnode.  We'll fill that subnode with the zero
-- tag, then we're done.
zeroPD : NatPD
zeroPD = ⟨ zz , ⋆ ⟩

-- Earlier we said suc had a subnode that gave you a thing.  The subnode is the
-- successor tag, the thing is the previous nat, then we're done.
sucPD : NatPD → NatPD
sucPD n = ⟨ ss , n , ⋆ ⟩

-- Adding an index to the Plain Description structure from before describes
-- inductive definitions in I → Set.  This means we need to specify the index
-- when asking for things now.
data Desc (I : Set) : Set₁ where
  -- Read field in A; continue with its value
  arg : (A : Set) → (A → Desc I) → Desc I
  -- Read a recursive subnode; continue regardless
  rec : I → Desc I → Desc I
  -- Stop reading.
  ret : I → Desc I

-- The indexed description of natural numbers.  As before, but from the ⊤ with
-- feeling this time.
NatDesc : Desc ⊤
NatDesc = arg NatT λ  { zz → ret ⋆ -- If zero, we're done here.
                      ; ss → rec ⋆ (ret ⋆) -- Otherwise we have a subnode that yields a predecessor.
                      }

-- Desugar into Agda-isms.
⟦_⟧ : {I : Set} → Desc I → (I → Set) → I → Set
⟦ (arg A D) ⟧ R i = Σ A λ a → ⟦ D a ⟧ R i
⟦ (rec h D) ⟧ R i = R h × ⟦ D ⟧ R i
⟦ (ret o) ⟧ R i = o ≡ i -- refl

-- The fixpoint of Indexed Data Descriptions is Indexed Data.
data Data {I : Set}(D : Desc I) : I → Set where
  ⟨_⟩ : ∀ {i} → ⟦ D ⟧ (Data D) i → Data D i

  -- The naturals in Indexed Data
Nat : Set
Nat = Data NatDesc ⋆

-- Earlier we said zero had a subnode.  We'll fill that subnode with the zero
-- tag, then we're done.
zeroD : Nat
zeroD = ⟨ zz , refl ⟩

-- Earlier we said suc had a subnode that gave you a thing.  The subnode is the
-- successor tag, the thing is the previous nat, then we're done.
sucD : Nat → Nat
sucD n = ⟨ ss , n , refl ⟩

-- With an index, we finally have enough structure to define "nontrivial"
-- structures like dependent Vectors.

-- The indexed description of a Vector Vec X n is given by:
VecDesc : Set → Desc Nat
VecDesc X = arg NatT λ  { -- If we have no elements we have nothing to give and 0 as an index.
                          zz → ret zeroD
                          -- If we have a cons cell, we have to yield the data in the cell and
                          -- the index.  The structure is thus
                          -- (successor tag, data, length, rest of vector, done)
                        ; ss → arg X (λ _ → arg Nat λ n → rec n (ret (sucD n)))
                        }

ListDesc : Set → Desc ⊤
ListDesc X = arg NatT λ { -- If we have no elements we have nothing to give and 0 as an index.
                        zz → ret ⋆
                        -- If we have a cons cell, we have to yield the data in the cell.
                        --  The structure is thus
                        -- (successor tag, data, rest of vector, done)
                        ; ss → arg X (λ _ → rec ⋆ (ret ⋆))
                        }

List : Set → Set
List X = Data (ListDesc X) _

nilL : ∀ {X} → List X
nilL = ⟨ zz , refl ⟩

consL : ∀ {X} → X → List X → List X
consL x xs = ⟨ ss , x , xs , refl ⟩

-- Naturally, we get an Indexed Data definition for Vectors indexed by n.
Vec : Set → Nat → Set
Vec X n = Data (VecDesc X) n

-- Earlier we said nil has nothing to give.
nil : ∀ {X} → Vec X zeroD
nil = ⟨ zz , refl ⟩

-- But cons has quite a bit more.  We need to fill the holes described in
-- VecDesc above.
consn : ∀ {n}{X} → X → Vec X n → Vec X (sucD n)
consn {n} x xs = ⟨ ss , x , n , xs , refl ⟩

-- "When presenting an inductive datatype as the least fixpoint
--
--     in : F (μF) → μF
--
-- of a suitable functor F : Set → Set, we provide the action of F on functions,
--  lifting operations on elements uniformly to operations on structures
--
--     map : (X → Y) → F X → F Y
--
-- and are rewarded with an iteration operator
--
-- fold : (F X → X) → μF → X
-- fold φ (in ds) → φ (map (fold φ) ds)
--
-- everywhere replacing in by φ. We can think of F as a signature, describing
-- how to build expressions from subexpressions, and μF as the syntactic
-- datatype of expressions so generated. A function φ : F X → X explains how to
-- implement each expression-form in the signature for values drawn from X we
-- say that φ is an F-algebra with carrier X. If we know how to implement the
-- signature, then we can evaluate expressions: that is exactly what fold does,
-- first using mapF to evaluate the subexpressions, then applying φ to deliver
-- the value of the whole."

-- Arrows are functions that respect indexing.  Not a fan of the notation here...
_⊆_ : ∀ {I} → (I → Set) → (I → Set) → Set
_⊆_ {I} X Y = {i : I} → X i → Y i
infix 40 _⊆_

-- Look, descriptions have a functorial action.
map : ∀ {I X Y} (D : Desc I) → (X ⊆ Y) → (⟦ D ⟧ X ⊆ ⟦ D ⟧ Y)
map (arg A D) f (a , d) = a , map (D a) f d
map (rec h D) f (x , d) = f x , map D f d
map (ret _) _ q = q

-- Shorthand for ⟦ Desc I ⟧ algebras so we don't have to carry around the index.
Alg : ∀ {I} → Desc I → (I → Set) → Set
Alg D X = ⟦ D ⟧ X ⊆ X

-- Conor's first definition makes the termination checker very angry.  This one
-- from larrytheliquid, however, does not
--  https://github.com/larrytheliquid/ornaments.
mutual
  fold : ∀ {I X} {D : Desc I} → (Alg D X) → Data D ⊆ X
  fold {D = D} φ ⟨ ds ⟩ = φ (map-fold D D φ ds)

  map-fold : ∀ {I X} (D′ D : Desc I) → (⟦ D′ ⟧ X ⊆ X) → ⟦ D ⟧ (Data D′) ⊆ ⟦ D ⟧ X
  map-fold D′ (arg A D) φ (a , ds) = a , map-fold D′ (D a) φ ds
  map-fold D′ (rec h D) φ (d , ds) = fold φ d , map-fold D′ D φ ds
  map-fold D′ (ret _) _ ds = ds

-- This looks mighty familiar to anybody who has used bananas and barbed wire to
-- get something done.
_+_ : Nat → Nat → Nat
x + y = fold (adda y) x where
  adda : Nat → Alg NatDesc (λ _ → Nat)
  adda y (zz , refl) = y
  adda y (ss , sum , refl) = sucD sum

-- But it generalizes to vectors too.
_++_ : ∀ {X m n} → Vec X m → Vec X n → Vec X (m + n)
xs ++ ys = fold (conca ys) xs where
  conca : ∀ {n X} → Vec X n → Alg (VecDesc X) (λ m → Vec X (m + n))
  conca ys (zz , refl) = ys
  conca ys (ss , x , m , conc , refl) = consn x conc

-- Suppose we have some description D : Desc I of an I-indexed family of
-- datatypes. Now suppose we come up with a more informative index set J,
-- together with some function e : J → I which erases this richer information.
-- Let us consider how we might develop a description D′ : Desc J which is
-- richer than D in an e-respecting way, so that we can always erase bits of a
-- Data D′ j to get an unadorned Data D (e j). For example, if we start with a
-- plain 1-indexed family, then e can only be !, the terminal arrow which always
-- returns ⋆.

-- In order to map I things to J things, we need a way of asking for the J
-- things that map to i through e.
data Inv {I J : Set} (e : J → I) : I → Set where
  inv : (j : J) → Inv e (e j)

-- Describes a way of ornamenting indexed descriptions.
data Orn {I : Set} (J : Set) (e : J → I) : Desc I → Set₁ where
  -- Binds A things to the Description.  Supposed to be untyped, but Agda hates
  -- that.  That may mean this or new can go away...
  arg : (A : Set) → {D : A → Desc I}  → ((a : A) → Orn J e (D a)) → Orn J e (arg A D)
  -- Takes the J that maps to our index I and a subnode ornament and tacks it
  -- onto the old ornament.
  rec : ∀ {i} {D : Desc I} → Inv e i → Orn J e D → Orn J e (rec i D)
  -- Tacks an ending onto the ornament.
  ret : ∀ {i} → Inv e i → Orn J e (ret i)
  -- Binds A things to the Description.
  new : {D : Desc I} → (A : Set) → (A → Orn J e D) → Orn J e D

-- With this kit, we can describe what it means to hang ornaments on a list.
ListOrn : Set → Orn ⊤ _ NatDesc
ListOrn X = arg NatT λ  { zz → ret (inv ⋆)
                        ; ss → new X (λ _ → rec (inv ⋆) (ret (inv ⋆)))
                        }

-- Ornaments have a forgetful map, but this time it drops all the
-- ornaments hanging off the description and sweeps them under the rug.
drop : ∀ {J I} {e : J → I} {D : Desc I} → Orn J e D → Desc J
-- To drop ornaments off an argument, return a reader that also drops ornaments.
drop (arg A O) = arg A (λ a → drop (O a))
-- For a "typed" argument do the same thing.
drop (new A O) = arg A (λ a → drop (O a))
-- For a subnode give up the right index and drop in the continuation.
drop (rec (inv j) O) = rec j (drop O)
-- Full Stop.
drop (ret (inv j)) = ret j

-- The ornamental algebra.
orna : ∀ {I J e} {D : Desc I} (O : Orn J e D) → Alg (drop O) (λ x → Data D (e x))
orna O ds = ⟨ erase O ds ⟩ where
  erase : ∀ {I J e} {D : Desc I} {R : I → Set} (O : Orn J e D) → ⟦ drop O ⟧ (λ x → R (e x)) ⊆ (λ x → ⟦ D ⟧ R (e x))
  erase (arg A O) (a , ds) = a , erase (O a) ds
  erase (rec (inv j) O) (d , ds) = d , erase O ds
  erase (ret (inv j)) refl = refl
  erase (new A O) (a , ds) = erase (O a) ds

-- A forgetful map generated for each ornament.
forget : ∀ {I J e} {D : Desc I} (O : Orn J e D) → Data (drop O) ⊆ (λ x → Data D (e x))
forget O = fold (orna O)

-- So you can recover descriptions by defining the Ornamental version and dropping
-- them all off.
List-Desc : Set → Desc ⊤
List-Desc X = drop (ListOrn X)

-- Unsurprisingly, Ornaments have an algebra.
algo : ∀ {I J} (D : Desc I) → Alg D J → Orn (Σ I J) fst D
algo (arg A Df) φ = arg A (λ a → algo (Df a) (λ x → φ (a , x)))
algo {J = J} (rec i D) φ = new (J i) (λ j → rec (inv (i , j)) (algo D (λ x → φ (j , x))))
algo (ret i) φ = ret (inv (i , φ refl))

-- To hang ornaments on vectors, one has to project the index out of it.
VecOrn : (X : Set) → Orn (⊤ × Nat) fst (List-Desc X)
VecOrn X = algo (List-Desc X) (orna (ListOrn X))