diff --git a/README.md b/README.md
index fa1c793250ad5c0c2d5468bc2b1abb46f8bca84f..22a9e87570c2bb60aa12a0182620b1b284de36bc 100644
--- a/README.md
+++ b/README.md
@@ -161,7 +161,7 @@ The deadline is **Friday, February 16, 2018**.
* [Effectful functional programming](slides/pedagand-01.pdf) ([Source](agda/01-effectful/Monad.lagda.rst)).
* [Dependent functional programming](slides/pedagand-02.pdf) ([Source](agda/02-dependent/Indexed.lagda.rst), [McCompiler.v](coq/McCompiler.v)).
* [Total functional programming](slides/pedagand-03.pdf) ([Source](agda/03-total/Recursion.lagda.rst)).
-* Generic functional programming.
+* ]Generic functional programming](slides/pedagand-04.pdf) ([Source](agda/04-generic/Desc.lagda.rst)).
* Open problems in dependent functional programming.
## Evaluation of the course
diff --git a/agda/04-generic/Desc.lagda.rst b/agda/04-generic/Desc.lagda.rst
new file mode 100644
index 0000000000000000000000000000000000000000..43101a91dbe2f5807cd0e1fb9232a35b9aa75bac
--- /dev/null
+++ b/agda/04-generic/Desc.lagda.rst
@@ -0,0 +1,1638 @@
+..
+ ::
+ {-# OPTIONS --allow-unsolved-metas --type-in-type #-}
+
+ module 04-generic.Desc where
+
+================================================================
+Generic functional programming
+================================================================
+
+Extensional vs. intensional generic programming:
+ - extensional: meta-level support for accessing structures
+ (intuition: type-classes)
+ - intensional: internalized code & interpretation
+ (intuition: universe)
+
+Extensional side of this lecture:
+ - (Lecture 1: Monad, MonadFail)
+ - Monoid
+ - Functor
+ - Applicative
+ - Foldable
+ - Traversable
+ - Want more? `Typeclassopedia`_!
+
+
+Intensional side of this lecture:
+ - reflecting inductive types
+ - internalized generic programming (over inductive types)
+
+Vision: `Generic programming is just programming `_
+ - Program with structure, one way (extensional) or another (intensional)
+ - Reflect the programming language in itself, one way (type-classes) or another (universe)
+
+Takeaways:
+ - you will be *able* to spot the following structures: Monoid, Functor, Applicative, Monad, Foldable, Traversable
+ - you will be *able* to generalize a program to exploit any of the above structures
+ - you will be *able* to program in/with a universe of descriptions
+ - you will be *familiar* with Naperian functors
+ - you will be *familiar* with the notion of universe
+ - you will be *familiar* with "instance arguments"/"type classes"
+
+************************************************
+Extensional Generic Programming
+************************************************
+
+..
+ ::
+ module Naperian where
+ open import Function
+
+ open import Data.Unit
+ open import Data.Bool
+ open import Data.Product hiding (map)
+ open import Data.Nat
+ open import Data.Fin hiding (_+_)
+ open import Data.List hiding (map ; replicate ; zipWith ; foldr ; sum ; sequence)
+
+ open import Relation.Binary.PropositionalEquality
+
+ infixr 5 _∷_
+ infixl 4 _<*>-Vec_
+
+
+
+Following Gibbons' `APLicative Programming Naperian Functors`_, we are
+going to study the algebraic structure of "array-oriented programming
+language", à la APL (or any of its descendant, such as J). In effect,
+we shall build a *deep embedding* of a (small) subset of APL in Agda.
+
+
+To do so, we will need a datastructure to represent multi-dimensional
+arrays, keeping track of (all of) their dimensions. We ought to be
+able to define:
+
+.. code-block:: agda
+
+ -- 3-elements vectors:
+ v123 = C (S (1 ∷ 2 ∷ 3 ∷ []))
+ v456 = C (S (4 ∷ 5 ∷ 6 ∷ []))
+
+ -- 2x2 matrices:
+ v12-34 = C (C (S (((1 ∷ 2 ∷ []) ∷
+ ((3 ∷ 4 ∷ []) ∷ [])))))
+
+ v56-78 = C (C (S (((5 ∷ 6 ∷ []) ∷
+ ((7 ∷ 8 ∷ []) ∷ [])))))
+
+ -- 3x3 matrix:
+ v123-456-789 = C (C (S ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ (4 ∷ 5 ∷ 6 ∷ []) ∷
+ (7 ∷ 8 ∷ 9 ∷ []) ∷ [])))
+
+ -- 3x2 matrix:
+ v12-45-78 = C (C (S ((1 ∷ 2 ∷ []) ∷
+ (4 ∷ 5 ∷ []) ∷
+ (7 ∷ 8 ∷ []) ∷ [])))
+
+ -- 2x3 matrix:
+ v123-456 = C (C (S ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ ((4 ∷ 5 ∷ 6 ∷ []) ∷ []))))
+
+ -- 2x2x2 matrix:
+ v1234-5678 = C (C (C (S (((1 ∷ 2 ∷ []) ∷
+ ((3 ∷ 4 ∷ []) ∷ [])) ∷
+ (((5 ∷ 6 ∷ []) ∷
+ ((7 ∷ 8 ∷ []) ∷ [])) ∷ [])))))
+
+Exploiting add-hoc polymorphism, we want to be able to apply unary
+operations pointwise to every element of a matrix, whatever its size:
+
+.. code-block:: agda
+
+ square (S 3) ≡ S 9
+ square v123 ≡ C (S (1 ∷ 4 ∷ 9 ∷ []))
+ square v123-456-789
+ ≡ C (C (S ((1 ∷ 4 ∷ 9 ∷ []) ∷
+ (16 ∷ 25 ∷ 36 ∷ []) ∷
+ (49 ∷ 64 ∷ 81 ∷ []) ∷ [])))
+ square v12-45-78
+ ≡ C (C (S(( 1 ∷ 4 ∷ []) ∷
+ (16 ∷ 25 ∷ []) ∷
+ (49 ∷ 64 ∷ []) ∷ [])))
+ square v1234-5678
+ ≡ C (C (C (S (((1 ∷ 4 ∷ []) ∷
+ ((9 ∷ 16 ∷ []) ∷ [])) ∷
+ (((25 ∷ 36 ∷ []) ∷
+ ((49 ∷ 64 ∷ []) ∷ [])) ∷ [])))))
+
+And similarly for n-ary operations, when the arguments are
+"compatible" (we will define and refine the notion of compatibility
+later):
+
+.. code-block:: agda
+
+ (_+_ <$> v123 ⊛ v456)
+ ≡ C (S (5 ∷ 7 ∷ 9 ∷ []))
+
+ (_+_ <$> v12-34 ⊛ v56-78)
+ ≡ C (C (S (( 6 ∷ 8 ∷ []) ∷
+ ((10 ∷ 12 ∷ []) ∷ []))))
+
+We should be able to process a matrix "per row", perhaps in a stateful
+manner:
+
+ .. code-block:: agda
+
+ sum v123 ≡ S 6
+ sum v123-456 ≡ C (S (6 ∷ 15 ∷ []))
+
+ sums v123 ≡ C (S (1 ∷ 3 ∷ 6 ∷ []))
+
+ sums v123-456 ≡ C (C (S ((1 ∷ 3 ∷ 6 ∷ []) ∷
+ (4 ∷ 9 ∷ 15 ∷ []) ∷ [])))
+
+Or "per column", using the *reranking* operator ```¹``, which amounts
+to pre- and post-compositing the desired operation with a
+transposition:
+
+ .. code-block:: agda
+
+ sums `¹ v123-456 ≡ C (C (S ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ (5 ∷ 7 ∷ 9 ∷ []) ∷ [])))
+
+
+--------------------------------
+Functor
+--------------------------------
+
+To represent vectors, we need a notion of arrays of a given size::
+
+ data Vec (A : Set) : ℕ → Set where
+ [] : Vec A zero
+ _∷_ : ∀ {n} (x : A) (xs : Vec A n) → Vec A (suc n)
+
+ vec : ℕ → Set → Set
+ vec n A = Vec A n
+
+Applying an operation pointwise to every elements of a vector is
+exactly what ``map`` does::
+
+ map-Vec : ∀ {n}{A B : Set} → (A → B) → vec n A → vec n B
+ map-Vec f [] = []
+ map-Vec f (x ∷ xs) = f x ∷ map-Vec f xs
+
+This would allow us to lift the operation ``square`` on numbers to
+apply on vectors of numbers.
+
+A function of type ``Set → Set`` having a ``map`` is called a `functor `_::
+
+ record Functor (F : Set → Set) : Set₁ where
+ infixl 4 _<$>_ _<$_
+
+ field
+ _<$>_ : ∀ {A B} → (A → B) → F A → F B
+
+ _<$_ : ∀ {A B} → A → F B → F A
+ x <$ y = const x <$> y
+
+ open Functor ⦃...⦄
+ instance
+ VecFunctor : ∀ {n} → Functor (vec n)
+ _<$>_ {{ VecFunctor {n} }} = map-Vec
+
+..
+ ::
+
+ module Example-vec-functor where
+ v123 : Vec ℕ 3
+ v123 = 1 ∷ 2 ∷ 3 ∷ []
+
+ v456 : Vec ℕ 3
+ v456 = 4 ∷ 5 ∷ 6 ∷ []
+
+ test1 : ((λ x → 3 + x) <$> v123) ≡ v456
+ test1 = refl
+
+
+It ought to abide by the functorial laws::
+
+ record IsFunctor (F : Set → Set){{_ : Functor F}} : Set₁ where
+ field
+ id-<$> : ∀ {A} (x : F A) →
+ (id <$> x) ≡ x
+ ∘-<$> : ∀ {A B C} (x : F A)(f : A → B)(g : B → C) →
+ ((g ∘ f) <$> x) ≡ (g <$> (f <$> x))
+
+**Exercise (difficulty: 1)** Prove the functor law for ``vec``.
+
+Another (arbitrary) example of functor is the following::
+
+ data Pair (A : Set) : Set where
+ P : A → A → Pair A
+
+ instance
+ PairFunctor : Functor Pair
+ _<$>_ {{PairFunctor}} f (P x y) = P (f x) (f y)
+
+**Exercise (difficulty: 1)** Prove the functor law for ``Pair``.
+
+**Exercise (difficulty: 1)** Show that lists define a functor.
+
+
+--------------------------------
+Applicative
+--------------------------------
+
+To lift n-ary operation ``f`` over two vectors of same size, we merely
+need a (total!) ``zipWith``::
+
+ zipWith-Vec : ∀ {n} {A B C : Set} →
+ (A → B → C) → vec n A → vec n B → vec n C
+ zipWith-Vec f [] [] = []
+ zipWith-Vec f (x ∷ xs) (y ∷ ys) = f x y ∷ zipWith-Vec f xs ys
+
+However, ``zipWith`` can be obtained from two more primitive
+operations and the functoriality of vectors::
+
+ replicate-Vec : ∀ {n} {A : Set} → A → vec n A
+ replicate-Vec {n = zero} x = []
+ replicate-Vec {n = suc n} x = x ∷ replicate-Vec x
+
+ _<*>-Vec_ : ∀ {n} {A B : Set} → vec n (A → B) → vec n A → vec n B
+ [] <*>-Vec [] = []
+ (f ∷ fs) <*>-Vec (x ∷ xs) = f x ∷ (fs <*>-Vec xs)
+
+ zipWith-Vec' : ∀ {n} {A B C : Set} →
+ (A → B → C) → vec n A → vec n B → vec n C
+ zipWith-Vec' f xs ys = f <$> xs <*>-Vec ys
+
+A functor equipped with these two operations is an `applicative
+functor `_::
+
+ record Applicative (F : Set → Set) : Set₁ where
+ infixl 4 _⊛_ _<⊛_ _⊛>_
+ infix 4 _⊗_
+
+ field
+ pure : ∀ {A} → A → F A
+ _⊛_ : ∀ {A B} → F (A → B) → F A → F B
+ overlap {{super}} : Functor F
+
+ zipWith : ∀ {A B C} → (A → B → C) → F A → F B → F C
+ zipWith f x y = f <$> x ⊛ y
+
+ _<⊛_ : ∀ {A B} → F A → F B → F A
+ a <⊛ b = const <$> a ⊛ b
+
+ _⊛>_ : ∀ {A B} → F A → F B → F B
+ a ⊛> b = (const id) <$> a ⊛ b
+
+ _⊗_ : ∀ {A B} → F A → F B → F (A × B)
+ x ⊗ y = (_,_) <$> x ⊛ y
+
+ replicate : ∀ {A} → A → F A
+ replicate = pure
+
+ open Applicative ⦃...⦄
+ instance
+ VecApplicative : ∀ {n} → Applicative (vec n)
+ pure {{VecApplicative}} = replicate-Vec
+ _⊛_ {{VecApplicative}} = _<*>-Vec_
+
+..
+ ::
+ module Example-vec-applicative where
+
+ open Example-vec-functor
+
+ v333 : Vec ℕ 3
+ v333 = replicate-Vec 3
+
+ test : zipWith _+_ v333 v123 ≡ v456
+ test = refl
+
+
+It ought to abide by the applicative laws::
+
+ record IsApplicative (F : Set → Set){{_ : Applicative F}} : Set₁ where
+ field
+ pure-id : ∀ {A} (v : F A) →
+ (pure id ⊛ v) ≡ v
+ pure-pure : ∀ {A B} (f : A → B)(a : A) →
+ (pure f ⊛ pure a) ≡ pure {F} (f a)
+ applicative : ∀ {A B}{u : F (A → B)}{a : A} →
+ (u ⊛ pure a) ≡ (pure (λ f → f a) ⊛ u)
+ composition : ∀ {A B C}{u : F (B → C)}{v : F (A → B)}{w : F A} →
+ (u ⊛ (v ⊛ w)) ≡ ((pure (λ g f a → g (f a))) ⊛ u ⊛ v ⊛ w)
+
+
+**Exercise (difficulty: 1)** Prove the applicative laws for ``vec``.
+
+Pairs are also applicative::
+
+ instance
+ PairApplicative : Applicative Pair
+ pure {{PairApplicative}} a = P a a
+ _⊛_ {{PairApplicative}} (P f g) (P x y) = P (f x) (g y)
+
+**Exercise (difficulty: 1)** Prove the applicative laws for ``Pair``.
+
+..
+ ::
+
+ open import Category.Monad
+ open import Category.Monad.State
+
+
+**Remark:** Every monad is an applicative functor (but not
+conversely!). So, for example, the ``State`` monad (encountered in
+Lecture 1) is an applicative::
+
+ instance
+ StateFunctor : ∀ {A : Set} → Functor (State A)
+ _<$>_ {{StateFunctor}} f m s = let (x , s') = m s in
+ f x , s'
+ StateApplicative : ∀ {A : Set} → Applicative (State A)
+ pure {{StateApplicative}} x s = x , s
+ _⊛_ {{StateApplicative}} fs xs s = let (f , s') = fs s in
+ let (x , s'') = xs s' in
+ f x , s''
+
+.. TODO: write the instances above (<$>, pure and ⊛) using the monadic operations
+
+**Exercise (difficulty: 1)** Write a program that takes a monad (specified with ``return`` and ``>>=``) and produces its underlying applicative.
+
+--------------------------------
+Naperian
+--------------------------------
+
+Let us (temporarily) model an m-by-n matrix as an m-elements vector of
+n-elements vectors::
+
+ matrix : ℕ → ℕ → Set → Set
+ matrix m n A = vec m (vec n A)
+
+..
+ ::
+ module Example-matrix where
+
+ m123-456 : matrix 2 3 ℕ
+ m123-456 = (1 ∷ 2 ∷ 3 ∷ []) ∷
+ (4 ∷ 5 ∷ 6 ∷ []) ∷ []
+
+
+To implement transposition (and, therefore, reranking), we need to
+access to be able to *index* into a vector (say, "get the value on row
+``i`` and column ``j``") as well as to be able to *create* a vector as
+a function from its indices (say, "define the matrix of value ``f(i,
+j)`` at row ``i`` and column ``j``). The first corresponds to a lookup
+while the second corresponds to a tabulation::
+
+ lookup-Vec : ∀ {n} {A : Set} → vec n A → Fin n → A
+ lookup-Vec (x ∷ xs) zero = x
+ lookup-Vec (x ∷ xs) (suc i) = lookup-Vec xs i
+
+ tabulate-Vec : ∀ {n} {A : Set} → (Fin n → A) → vec n A
+ tabulate-Vec {zero} f = []
+ tabulate-Vec {suc n} f = f zero ∷ tabulate-Vec (f ∘ suc)
+
+ transpose-Matrix : ∀ {m n} {A : Set} → matrix m n A → matrix n m A
+ transpose-Matrix m = tabulate-Vec (λ i →
+ tabulate-Vec (λ j →
+ lookup-Vec (lookup-Vec m j) i))
+
+..
+ ::
+ module Example-matrix-tranpose where
+
+ open Example-matrix
+
+ test : transpose-Matrix m123-456
+ ≡ (1 ∷ 4 ∷ []) ∷
+ (2 ∷ 5 ∷ []) ∷
+ (3 ∷ 6 ∷ []) ∷ []
+ test = refl
+
+An applicative functor such that there exists a set ``Log`` supporting
+``lookup`` and ``tabulate`` is called a Naperian functor or a
+`representable functor`_::
+
+ record Naperian (F : Set → Set) : Set₁ where
+ field
+ Log : Set
+ lookup : ∀ {A} → F A → (Log → A)
+ tabulate : ∀ {A} → (Log → A) → F A
+ overlap {{super}} : Applicative F
+
+ positions : F Log
+ positions = tabulate λ ix → ix
+
+ open Naperian {{...}}
+
+ instance
+ VecNaperian : ∀ {n} → Naperian (vec n)
+ Log {{VecNaperian {n}}} = Fin n
+ lookup {{VecNaperian}} = lookup-Vec
+ tabulate {{VecNaperian}} = tabulate-Vec
+
+.. TODO: add `comonad instance `_
+
+
+**Exercise (difficulty: 2)** State the Naperian laws and prove them
+for vectors.
+
+Pairs are Naperian too::
+
+ instance
+ PairNaperian : Naperian Pair
+ Log {{PairNaperian}} = Bool
+ lookup {{PairNaperian}} (P x y) true = x
+ lookup {{PairNaperian}} (P x y) false = y
+ tabulate {{PairNaperian}} f = P (f true) (f false)
+
+
+Given any pair of Naperian functors, transposition is expressed as
+swapping the composition of structures::
+
+ transpose : ∀ {F G : Set → Set}
+ {{_ : Naperian F}}{{_ : Naperian G}} →
+ ∀ {A} → F (G A) → G (F A)
+ transpose fga = tabulate <$> (tabulate (λ gx fx → lookup (lookup fga fx) gx))
+
+..
+ ::
+
+ module Example-matrix-tranpose' where
+
+ open Example-matrix
+
+ test : transpose m123-456
+ ≡ (1 ∷ 4 ∷ []) ∷
+ (2 ∷ 5 ∷ []) ∷
+ (3 ∷ 6 ∷ []) ∷ []
+ test = refl
+
+ pv123-456 : Pair (vec 3 ℕ)
+ pv123-456 = P (1 ∷ 2 ∷ 3 ∷ [])
+ (4 ∷ 5 ∷ 6 ∷ [])
+
+ test2 : transpose pv123-456 ≡ P 1 4 ∷ P 2 5 ∷ P 3 6 ∷ []
+ test2 = refl
+
+
+--------------------------------
+Interlude: Monoid
+--------------------------------
+
+So far, we have focused our attention onto type constructors
+(functions of type ``Set → Set`` ). But sets can be interesting
+too. For example, we may be interested in exhibiting the monoidal
+structure of a given set::
+
+ record Monoid (A : Set) : Set₁ where
+ infixr 6 _<>_
+ field
+ mempty : A
+ _<>_ : A → A → A
+
+ open Monoid ⦃...⦄
+
+
+Famous monoids include ``(ℕ, 0, _+_)`` and ``(List A, [], _++_)``
+(also called the free monoid)::
+
+ instance
+ NatMonoid : Monoid ℕ
+ mempty {{NatMonoid}} = 0
+ _<>_ {{NatMonoid}} = _+_
+
+ ListMonoid : ∀ {A} → Monoid (List A)
+ mempty {{ListMonoid}} = []
+ _<>_ {{ListMonoid}} xs ys = xs ++ ys
+
+Perhaps less obviously (or, perhaps, too obviously to be noted),
+endomorphisms form a monoid ``(A → A, id, _∘_)``::
+
+ EndoMonoid : ∀ {A} → Monoid (A → A)
+ mempty {{EndoMonoid}} = id
+ _<>_ {{EndoMonoid}} f g = f ∘ g
+
+**Exercise (difficulty: 2)** State the monoid laws and prove them for
+the above examples.
+
+
+--------------------------------
+Foldable
+--------------------------------
+
+To compute the running ``sum`` over a vector of numbers, we need a
+notion of iteration over vectors. In all generality, the left-to-right
+iteration over a vector can be implemented as the interpretation into
+a given monoid::
+
+ foldMap-Vec : ∀ {n}{A}{W : Set} {{MonW : Monoid W}} → (A → W) → vec n A → W
+ foldMap-Vec f [] = mempty
+ foldMap-Vec f (x ∷ xs) = f x <> foldMap-Vec f xs
+
+ sumAll-Vec : ∀ {n} → vec n ℕ → ℕ
+ sumAll-Vec = foldMap-Vec id
+
+Note that we recover the 70's embodiment of iteration, the ``foldr``,
+by exploiting the fact that endomorphisms form a monoid::
+
+ foldr-Vec : ∀ {n}{A B : Set} → (A → B → B) → B → vec n A → B
+ foldr-Vec su ze fs = foldMap-Vec su fs ze
+
+Conversely, we can interpret it into the initial model of foldability,
+namely lists::
+
+ toList-Vec : ∀ {n A} → vec n A → List A
+ toList-Vec = foldMap-Vec (λ a → a ∷ [])
+
+..
+ ::
+ module Example-sumAll where
+ open Example-vec-functor
+
+ test-sum-vec : sumAll-Vec v123 ≡ 6
+ test-sum-vec = refl
+
+ test-toList-vec : toList-Vec v123 ≡ 1 ∷ 2 ∷ 3 ∷ []
+ test-toList-vec = refl
+
+
+A functor offering such an iterator is said to be `foldable
+`_::
+
+ record Foldable (F : Set → Set) : Set₁ where
+ field
+ foldMap : ∀ {A}{W : Set} {{MonW : Monoid W}} → (A → W) → F A → W
+ overlap {{super}} : Functor F
+
+ foldr : ∀ {A B : Set} → (A → B → B) → B → F A → B
+ foldr su ze fs = foldMap su fs ze
+
+ toList : ∀ {A} → F A → List A
+ toList = foldMap (λ a → a ∷ [])
+
+ open Foldable {{...}}
+
+ sumAll : ∀ {F} → {{ _ : Foldable F}} → F ℕ → ℕ
+ sumAll = foldMap id
+
+ instance
+ VecFoldable : ∀ {n} → Foldable (λ A → Vec A n)
+ foldMap {{VecFoldable}} = foldMap-Vec
+
+Pairs are foldable too::
+
+ instance
+ PairFoldable : Foldable Pair
+ foldMap {{PairFoldable}} f (P a b) = f a <> f b
+
+**Exercise (difficulty: 1)** Show that lists are foldable.
+
+
+..
+ ::
+ module Example-pair-foldable where
+
+ test-toList-pair : toList (P 42 24) ≡ 42 ∷ 24 ∷ []
+ test-toList-pair = refl
+
+ test-sum-pair : sumAll (P 42 24) ≡ 66
+ test-sum-pair = refl
+
+**Exercise (difficulty: 2)** State the foldable laws and prove them for
+the above examples.
+
+--------------------------------
+Traversable
+--------------------------------
+
+Being foldable enables us to write pure iterators. To compute the
+running sum of a vector, we need to perform a stateful
+iteration::
+
+ traverse-Vec : ∀ {n F A B} {{_ : Applicative F}} → (A → F B) → vec n A → F (vec n B)
+ traverse-Vec f [] = pure []
+ traverse-Vec f (x ∷ v) = _∷_ <$> f x ⊛ traverse-Vec f v
+
+ increase : ℕ → State ℕ ℕ
+ increase n = λ m → let n' = m + n in n' , n'
+
+ sumsAll-Vec : ∀ {n} → vec n ℕ → vec n ℕ
+ sumsAll-Vec xs = proj₁ (traverse-Vec increase xs 0)
+
+..
+ ::
+ module Example-Traversable where
+ open Example-vec-functor
+
+ test-v136 : sumsAll-Vec v123 ≡ 1 ∷ 3 ∷ 6 ∷ []
+ test-v136 = refl
+
+
+**Remark:** Rather than an applicative, we could have asked for a
+monad. However, this is needlessly restrictive (remember, every monad
+is an applicative): if the side-effects are commutative (and we like
+those for `performance reasons `_), we
+get more freedom with a purely applicative implementation rather than
+a monadic one (for the same reason that OCaml is applicative, compiler
+writers like under-specifications!).
+
+A functor offering such an iterator is said to be `traversable
+`_::
+
+ record Traversable (T : Set → Set) : Set₁ where
+ field
+ traverse : ∀ {F : Set → Set} {A B} {{_ : Applicative F}} → (A → F B) → T A → F (T B)
+ overlap {{super}} : Foldable T
+
+ sequence : ∀ {F : Set → Set} {A} {{_ : Applicative F}} → T (F A) -> F (T A)
+ sequence = traverse id
+
+ open Traversable ⦃...⦄
+ instance
+ VectorTraversable : ∀ {n} → Traversable (λ A → Vec A n)
+ traverse {{VectorTraversable}} f [] = pure []
+ traverse {{VectorTraversable}} f (x ∷ v) = _∷_ <$> f x ⊛ traverse f v
+
+Surprise, pairs are traversable too::
+
+ instance
+ PairTraversable : Traversable Pair
+ traverse {{PairTraversable}} f (P x y) = P <$> f x ⊛ f y
+
+**Exercise (difficulty: 2)** State the foldable laws and prove them for
+the above examples.
+
+The running sum example can then be implemented for any traversable
+structure::
+
+ sumsAll : ∀ {T} {{_ : Traversable T}} → T ℕ → T ℕ
+ sumsAll xs = proj₁ (traverse increase xs 0)
+
+..
+ ::
+ module Example-sumsAll where
+ open Example-vec-functor hiding (test1)
+
+ test1 : sumsAll v123 ≡ 1 ∷ 3 ∷ 6 ∷ []
+ test1 = refl
+
+ test2 : sumsAll (P 1 2) ≡ P 1 3
+ test2 = refl
+
+--------------------------------
+Dimension
+--------------------------------
+
+To serve as a data container, we thus require for our type constructor
+to be both traversable (ie. support effectful iteration) and naperian
+(ie. suppport indexing)::
+
+ record Dimension (F : Set → Set) : Set₁ where
+ field
+ overlap {{super₁}} : Traversable F
+ overlap {{super₂}} : Naperian F
+
+ size : ∀ {α} → F α → ℕ
+ size as = length (toList as)
+
+ open Dimension ⦃...⦄
+
+As a result of our hard work, pairs and vectors are straightforward
+instances::
+
+ instance
+ PairDimension : Dimension Pair
+ PairDimension = record {}
+
+ VectorDimension : ∀ {n} → Dimension (vec n)
+ VectorDimension = record {}
+
+**Remark:** Any dimensionable functor admits a ``size`` operation,
+which counts the number of elements stored in the structure. For
+vectors, a direct implementation of ``size`` would simply return the
+index of the vector (without conversion to list) and for pairs, it is
+constantly equal to 2.
+
+**Example: binary vectors** rather than indexing vectors by Peano
+numbers, we can index them by binary numbers::
+
+ data Binary : Set where
+ zero : Binary
+ 2× : Binary → Binary
+ 1+2× : Binary → Binary
+
+ data BVector (A : Set) : Binary → Set where
+ single : A → BVector A zero
+ join : ∀ {n} → BVector A n → BVector A n → BVector A (2× n)
+ 1+join : ∀ {n} → A → BVector A n → BVector A n → BVector A (1+2× n)
+
+ bvector : Binary → Set → Set
+ bvector b A = BVector A b
+
+**Exercise (difficulty: 2)** Show that binary vectors can be used as a
+dimension::
+
+ instance
+ BVectorFunctor : ∀ {n} → Functor (bvector n)
+ BVectorFunctor = {!!}
+
+ BVectorFoldable : ∀ {n} → Foldable (bvector n)
+ BVectorFoldable = {!!}
+
+ BVectorNaperian : ∀ {n} → Naperian (bvector n)
+ BVectorNaperian = {!!}
+
+ BVectorTraversable : ∀ {n} → Traversable (bvector n)
+ BVectorTraversable = {!!}
+
+ BVectorDimension : ∀ {n} → Dimension (bvector n)
+ BVectorDimension = record {}
+
+**Remark:** as for vectors, the ``size`` of a binary vector can be
+statically deduced from the index::
+
+ bin2nat : Binary → ℕ
+ bin2nat zero = 0
+ bin2nat (2× b) = 2 * (bin2nat b)
+ bin2nat (1+2× b) = 1 + 2 * bin2nat b
+
+**Example: block matrices** This example is taken from `An agda
+formalisation of the transitive closure of block matrices`_, in which
+block matrices are defined as follows::
+
+ data Shape : Set where
+ L : Shape
+ B : Shape → Shape → Shape
+
+ data M (a : Set) : (rows cols : Shape) → Set where
+ One : a → M a L L
+ Row : {c₁ c₂ : Shape} →
+ M a L c₁ → M a L c₂ → M a L (B c₁ c₂)
+ Col : {r₁ r₂ : Shape} →
+ M a r₁ L → M a r₂ L → M a (B r₁ r₂) L
+ Q : {r₁ r₂ c₁ c₂ : Shape} →
+ M a r₁ c₁ → M a r₁ c₂ →
+ M a r₂ c₁ → M a r₂ c₂ →
+ M a (B r₁ r₂) (B c₁ c₂)
+
+**Exercise (difficulty: 2)** Show that block matrices can be used as a
+dimension::
+
+ instance
+ MFunctor : ∀ {r c} → Functor (λ A → M A r c)
+ MFunctor = {!!}
+
+ MFoldable : ∀ {r c} → Foldable (λ A → M A r c)
+ MFoldable = {!!}
+
+ MNaperian : ∀ {r c} → Naperian (λ A → M A r c)
+ MNaperian = {!!}
+
+ MTraversable : ∀ {r c} → Traversable (λ A → M A r c)
+ MTraversable = {!!}
+
+ MDimension : ∀ {r c} → Dimension (λ A → M A r c)
+ MDimension = record {}
+
+**Exercise (difficulty: 2)** Show that the generic ``size`` operator
+defined by ``MDimension`` is equivalent to the following function::
+
+ toNat : Shape → ℕ
+ toNat L = 1
+ toNat (B l r) = toNat l + toNat r
+
+
+Programming solely with the structured offered by dimensions, we can
+implement a generic inner product and matrix product::
+
+ inner-product : ∀ {F} → {{_ : Dimension F}} →
+ F ℕ → F ℕ → ℕ
+ inner-product xs ys = sumAll (zipWith _*_ xs ys)
+
+ matrix-product : ∀ {F G H} →
+ {{_ : Dimension F}}{{_ : Dimension G}}{{_ : Dimension H}} →
+ F (G ℕ) → G (H ℕ) → F (H ℕ)
+ matrix-product {F}{G}{H} {{dimF}} xss yss =
+ zipWith (zipWith inner-product) (replicate <$> xss) (replicate (transpose yss))
+
+..
+ ::
+ module Example-product where
+ open Example-vec-functor
+
+ test : inner-product v123 v456 ≡ 32
+ test = refl
+
+ test2 : inner-product (P 1 2) (P 4 5) ≡ 14
+ test2 = refl
+
+ m12-34-56 : matrix 3 2 ℕ
+ m12-34-56 = (1 ∷ 2 ∷ []) ∷
+ (3 ∷ 4 ∷ []) ∷
+ (5 ∷ 6 ∷ []) ∷ []
+
+ m6789-1234 : matrix 2 4 ℕ
+ m6789-1234 = (6 ∷ 7 ∷ 8 ∷ 9 ∷ []) ∷
+ (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) ∷ []
+
+ test3 : matrix-product m12-34-56 m6789-1234
+ ≡ (8 ∷ 11 ∷ 14 ∷ 17 ∷ []) ∷
+ (22 ∷ 29 ∷ 36 ∷ 43 ∷ []) ∷
+ (36 ∷ 47 ∷ 58 ∷ 69 ∷ []) ∷ []
+ test3 = refl
+
+--------------------------------
+Multi-dimensional matrices
+--------------------------------
+
+So far, we have mostly equipped vectors with structure (and pretended
+that we cared about ``Pair``). To talk about m-by-n matrices, we ended
+up defining a custom datatype built from vectors of vectors. In this
+section, we are going to generalize matrices both in terms of
+dimension (the number of functors composed) and Dimension (the type of
+functors that are composed).
+
+This is also were all the unification hell breaks loose. This means
+that we are going to introduce apparently useless definitions to guide
+the unifier and some manual instanciations here and there.
+
+A high-dimensional matrix is essentially a composition of multiple
+Dimension functors. To help the unifier, we are going to reify the
+composition (and identity) through custom datatype definitions::
+
+ data Id (A : Set) : Set where
+ I : A → Id A
+
+ data Seq (G : Set → Set)(F : Set → Set)(A : Set) : Set where
+ S : F (G A) → Seq G F A
+
+Unsurprisingly, the structures we have seen so far are verified by the
+identity functor and closed under composition, so we get the expected
+instances.
+
+..
+ ::
+
+ instance
+ IdFunctor : Functor Id
+ _<$>_ {{IdFunctor}} f (I x) = I (f x)
+
+ IdApplicative : Applicative Id
+ pure {{IdApplicative}} a = I a
+ _⊛_ {{IdApplicative}} (I f) (I x) = I (f x)
+
+ IdNaperian : Naperian Id
+ Log {{IdNaperian}} = ⊤
+ lookup {{IdNaperian}} (I x) tt = x
+ tabulate {{IdNaperian}} f = I (f tt)
+
+ IdFoldable : Foldable Id
+ foldMap {{IdFoldable}} f (I a) = f a
+
+ IdTraversable : Traversable Id
+ traverse {{IdTraversable}} f (I x) = I <$> f x
+
+ IdDimension : Dimension Id
+ IdDimension = record {}
+
+ SeqFunctor : ∀ {F G} → {{_ : Functor F}}{{ _ : Functor G}} →
+ Functor (Seq F G)
+ _<$>_ {{SeqFunctor}} f (S fga) = S ((_<$>_ f) <$> fga)
+
+ SeqApplicative : ∀ {F G} → {{_ : Applicative F}}{{ _ : Applicative G}} →
+ Applicative (Seq F G)
+ pure {{SeqApplicative}} a = S (pure (pure a))
+ _⊛_ {{SeqApplicative {F}{G} }} (S fgf) (S fga) = S (_⊛_ <$> fgf ⊛ fga)
+
+ SeqFoldable : ∀ {F G} → {{_ : Foldable F}}{{ _ : Foldable G}} →
+ Foldable (Seq F G)
+ foldMap {{SeqFoldable}} rec (S fga) = foldMap (foldMap rec) fga
+
+ SeqTraversable : ∀ {F G} → {{_ : Traversable F}}{{ _ : Traversable G}} →
+ Traversable (Seq F G)
+ traverse {{SeqTraversable}} f (S fga) = S <$> traverse (traverse f) fga
+
+ SeqNaperian : ∀ {F G} → {{_ : Naperian F}}{{ _ : Naperian G}} → Naperian (Seq F G)
+ Log {{SeqNaperian {{naperianF}} {{naperianG}} }} = Log {{naperianG}} × Log {{naperianF}}
+ lookup {{SeqNaperian}} (S fga) (lf , lg) = lookup (lookup fga lf) lg
+ tabulate {{SeqNaperian {{naperianF}}{{naperianG}}}} f = S (tabulate (λ lf → tabulate (λ lg → f (lf , lg))))
+
+ SeqDimension : ∀ {F G} → {{ _ : Dimension F}}{{ _ : Dimension G}} →
+ Dimension (Seq F G)
+ SeqDimension = record {}
+
+An hyper-matrix is essentially a list of functors::
+
+ hyper : Set₁
+ hyper = List (Set → Set)
+
+which is interpreted as-is in the monoid of endofunctor on ``Set``::
+
+ Hyper : hyper → Set → Set
+ Hyper [] A = Id A
+ Hyper (F ∷ Fs) A = Seq F (Hyper Fs) A
+
+that is (but this would play nice with unification):
+
+.. code-block:: agda
+
+ Hyper : hyper → Set → Set
+ Hyper Fs A = foldMap {{_}}{{FunctorMonoid}} id Fs A
+ where FunctorMonoid : Monoid (Set → Set)
+ mempty {{FunctorMonoid}} = Id
+ _<>_ {{FunctorMonoid}} = Seq
+
+..
+ ::
+ module Example-hyper where
+
+``Hyper`` thus provides a uniform way to type high-dimension
+matrices::
+
+ v123 : Hyper (vec 3 ∷ []) ℕ
+ v123 = S (I (1 ∷ 2 ∷ 3 ∷ []))
+
+ v456 : Hyper (vec 3 ∷ []) ℕ
+ v456 = S (I (4 ∷ 5 ∷ 6 ∷ []))
+
+ v123-456-789 : Hyper (vec 3 ∷ vec 3 ∷ []) ℕ
+ v123-456-789 = S (S (I ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ (4 ∷ 5 ∷ 6 ∷ []) ∷
+ (7 ∷ 8 ∷ 9 ∷ []) ∷ [])))
+
+ v12-45-78 : Hyper (vec 2 ∷ vec 3 ∷ []) ℕ
+ v12-45-78 = S (S (I ((1 ∷ 2 ∷ []) ∷
+ (4 ∷ 5 ∷ []) ∷
+ (7 ∷ 8 ∷ []) ∷ [])))
+
+ m1234 : Hyper (vec 2 ∷ vec 2 ∷ []) ℕ
+ m1234 = S (S (I (((1 ∷ 2 ∷ []) ∷
+ ((3 ∷ 4 ∷ []) ∷ [])))))
+
+ m5678 : Hyper (vec 2 ∷ vec 2 ∷ []) ℕ
+ m5678 = S (S (I (((5 ∷ 6 ∷ []) ∷
+ ((7 ∷ 8 ∷ []) ∷ [])))))
+
+ v1234-5678 : Hyper (vec 2 ∷ vec 2 ∷ vec 2 ∷ []) ℕ
+ v1234-5678 = S (S (S (I (((1 ∷ 2 ∷ []) ∷
+ ((3 ∷ 4 ∷ []) ∷ [])) ∷
+ (((5 ∷ 6 ∷ []) ∷
+ ((7 ∷ 8 ∷ []) ∷ [])) ∷ [])))))
+
+ v123-456 : Hyper (vec 3 ∷ vec 2 ∷ []) ℕ
+ v123-456 = S (S (I ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ ((4 ∷ 5 ∷ 6 ∷ []) ∷ []))))
+
+
+While we can try to *inhabit* an hyper-matrix for **any** list of
+functors, we will only be able to *compute* with those when each of
+these functors are Dimensions::
+
+ Shapely : List (Set → Set) → Set₁
+ Shapely [] = ⊤
+ Shapely (F ∷ Fs) = Dimension F × Shapely Fs
+
+.. XXX: guide the unifier to automatically proof-search witnesses of ``Shapely``
+ ::
+ instance
+ ShapelyNil : Shapely []
+ ShapelyNil = tt
+
+ ShapelyCons : ∀ {F Fs} → {{_ : Dimension F}}{{ _ : Shapely Fs}} → Shapely (F ∷ Fs)
+ ShapelyCons {{dimF}} {{shapeFs}} = dimF , shapeFs
+
+As a result, a shapely list of functors is itself a dimension.
+
+
+
+**Exercise (difficulty: 3)** Show that a shapely hyper-matrix has a dimension::
+
+ HyperFunctor : ∀ {Fs} → Shapely Fs → Functor (Hyper Fs)
+ HyperFunctor shapes = {!!}
+
+ HyperApplicative : ∀ {Fs} → Shapely Fs → Applicative (Hyper Fs)
+ HyperApplicative shapes = {!!}
+
+ HyperNaperian : ∀ {Fs} → Shapely Fs → Naperian (Hyper Fs)
+ HyperNaperian shapes = {!!}
+
+ HyperFoldable : ∀ {Fs} → Shapely Fs → Foldable (Hyper Fs)
+ HyperFoldable shapes = {!!}
+
+ HyperTraversable : ∀ {Fs} → Shapely Fs → Traversable (Hyper Fs)
+ HyperTraversable shapes = {!!}
+
+ HyperDimension : ∀ {Fs} → Shapely Fs → Dimension (Hyper Fs)
+ HyperDimension shapes = {!!}
+
+
+
+As a result, we can define::
+
+ square : ∀ {T} → {{_ : Traversable T}} → T ℕ → T ℕ
+ square x = (λ x → x * x) <$> x
+
+and seamlessly apply it to any hyper-matrix.
+
+We can also define the generalized running sum::
+
+ sums : ∀ {F Fs}
+ {{_ : Shapely Fs}}{{_ : Dimension F}} →
+ Hyper (F ∷ Fs) ℕ → Hyper (F ∷ Fs) ℕ
+ sums {{shapeFs}} (S xs) = S (sumsAll <$>H xs)
+ where open Functor (HyperFunctor shapeFs) renaming (_<$>_ to _<$>H_)
+
+and apply it to any matrix of dimension at least ``F``.
+
+..
+ ::
+ module Example-dimension where
+ open Example-hyper
+
+ example1 : square (I 3) ≡ I 9
+ example1 = refl
+
+ example2 : square v123 ≡ S (I (1 ∷ 4 ∷ 9 ∷ []))
+ example2 = refl
+
+
+ example3 : square v123-456-789
+ ≡ S (S (I (( 1 ∷ 4 ∷ 9 ∷ []) ∷
+ (16 ∷ 25 ∷ 36 ∷ []) ∷
+ (49 ∷ 64 ∷ 81 ∷ []) ∷ [])))
+ example3 = refl
+
+ example4 : square v12-45-78
+ ≡ S (S (I ((1 ∷ 4 ∷ []) ∷
+ (16 ∷ 25 ∷ []) ∷
+ (49 ∷ 64 ∷ []) ∷ [])))
+ example4 = refl
+
+
+ example5 : square v1234-5678
+ ≡ S (S (S (I (((1 ∷ 4 ∷ []) ∷
+ ((9 ∷ 16 ∷ []) ∷ [])) ∷
+ (((25 ∷ 36 ∷ []) ∷
+ ((49 ∷ 64 ∷ []) ∷ [])) ∷ [])))))
+ example5 = refl
+
+ example6 : (_+_ <$> v123 ⊛ v456)
+ ≡ S (I (5 ∷ 7 ∷ 9 ∷ []))
+ example6 = refl
+
+ example7 : (_+_ <$> m1234 ⊛ m5678)
+ ≡ S (S (I (( 6 ∷ 8 ∷ []) ∷
+ ((10 ∷ 12 ∷ []) ∷ []))))
+ example7 = refl
+
+ example10 : sums v123
+ ≡ S (I (1 ∷ 3 ∷ 6 ∷ []))
+ example10 = refl
+
+ example11 : sums v123-456
+ ≡ S (S (I ((1 ∷ 3 ∷ 6 ∷ []) ∷
+ (4 ∷ 9 ∷ 15 ∷ []) ∷ [])))
+ example11 = refl
+
+
+We can also iterate over all "rows" of an hyper-matrix, bringing the
+dimension down by ``F``::
+
+ reduceBy : ∀ {F Fs A M} →
+ {{_ : Shapely Fs}}{{_ : Monoid M}}{{_ : Dimension F}} →
+ (A → M) → Hyper (F ∷ Fs) A → Hyper Fs M
+ reduceBy {{shapeFs}} f (S fga) = (foldMap f) <$>H fga
+ where open Functor (HyperFunctor shapeFs) renaming (_<$>_ to _<$>H_)
+
+ sum : ∀ {F Fs} →
+ {{_ : Shapely Fs}}{{_ : Dimension F}} →
+ Hyper (F ∷ Fs) ℕ → Hyper Fs ℕ
+ sum = reduceBy id
+
+..
+ ::
+ module Example-reduceBy where
+ open Example-hyper
+
+ example8 : sum v123 ≡ I 6
+ example8 = refl
+
+
+ example9 : sum v123-456 ≡ S (I (6 ∷ 15 ∷ []))
+ example9 = refl
+
+And, finally, we can generalize ``transpose`` to any hyper-matrix and
+obtain the reranking operator::
+
+ transpose' : ∀ {A F G Fs} →
+ {{_ : Shapely Fs}}{{_ : Dimension F}}{{_ : Dimension G}} →
+ Hyper (F ∷ G ∷ Fs) A → Hyper (G ∷ F ∷ Fs) A
+ transpose' {{shapeFs}} (S (S x)) = S (S (transpose <$>H x))
+ where open Functor (HyperFunctor shapeFs) renaming (_<$>_ to _<$>H_)
+
+ _`¹_ : ∀ {A F₁ F₂ Fs G₁ G₂ Gs} →
+ {{_ : Shapely Fs}}{{_ : Shapely Gs}} →
+ {{_ : Dimension F₁}}{{_ : Dimension F₂}}
+ {{_ : Dimension G₁}}{{_ : Dimension G₂}} →
+ (Hyper (F₁ ∷ F₂ ∷ Fs) A → Hyper (G₁ ∷ G₂ ∷ Gs) A) →
+ Hyper (F₂ ∷ F₁ ∷ Fs) A → Hyper (G₂ ∷ G₁ ∷ Gs) A
+ f `¹ m = transpose' (f (transpose' m))
+
+..
+ ::
+
+ module test where
+ open Example-hyper
+
+ example12a : transpose' v123-456
+ ≡ S (S (I ((1 ∷ (4 ∷ [])) ∷
+ ((2 ∷ (5 ∷ [])) ∷
+ (3 ∷ (6 ∷ [])) ∷ []))))
+ example12a = refl
+
+ example12b : transpose' v1234-5678
+ ≡ S (S (S (I (((1 ∷ (3 ∷ [])) ∷
+ ((2 ∷ (4 ∷ [])) ∷ [])) ∷
+ (((5 ∷ (7 ∷ [])) ∷
+ ((6 ∷ (8 ∷ [])) ∷ [])) ∷ [])))))
+ example12b = refl
+
+ example12 : sums `¹ v123-456 ≡ S (S (I ((1 ∷ 2 ∷ 3 ∷ []) ∷
+ (5 ∷ 7 ∷ 9 ∷ []) ∷ [])))
+ example12 = refl
+
+
+At this stage, we are merely touching upon what Gibbons' talks about
+in `APLicative Programming Naperian Functors`_. For instance, when
+applying a binary operation, we (that is, applicative) currently ask
+for the two argument matrices to be exactly the same. J, on the other
+hand, would automatically lift values to match up dimensions. For
+example, we would like to able to sum a scalar to a matrix:
+
+.. code-block:: agda
+
+ I 3 + S (I (4 ∷ 5 ∷ 6 ∷ []))
+ ≡ S (I (3 ∷ 3 ∷ 3 ∷ [])) + S (I (4 ∷ 5 ∷ 6 ∷ []))
+ ≡ S (I (7 ∷ 8 ∷ 9 ∷ []))
+
+ S (I (1 ∷ 2 ∷ 3 ∷ [])) + S (S (I ((4 ∷ 5 ∷ 6 ∷ []) ∷
+ (7 ∷ 8 ∷ 9 ∷ []) ∷ [])))
+ ≡ S (S (I (1 ∷ 2 ∷ 3 ∷ []) ∷
+ (1 ∷ 2 ∷ 3 ∷ []) ∷ []))
+ + S (S (I ((4 ∷ 5 ∷ 6 ∷ []) ∷
+ (7 ∷ 8 ∷ 9 ∷ []) ∷ [])))
+ ≡ S (S (I ((5 ∷ 7 ∷ 9 ∷ []) ∷
+ (8 ∷ 10 ∷ 12 ∷ []) ∷ [])))
+
+
+However, this is also at this point that the extensional style starts
+to break. To feel that pain, try to translate Gibbons' ``Max``
+type-class. As we will see in the last lecture, manipulating an object
+of type ``List (Set → Set)`` is a red-herring, it is already quite
+surprising that we came this far.
+
+
+************************************************
+Intensional Generic Programming
+************************************************
+..
+ ::
+ module Intensional where
+ open import Function
+
+ open import Data.Unit
+ open import Data.Bool
+ open import Data.Product hiding (map)
+ open import Data.Sum hiding (map)
+ open import Data.Nat hiding (fold)
+ open import Data.Fin renaming (suc to sucF) hiding (fold)
+ open import Data.Vec hiding (map)
+
+ open import Induction
+
+ open import Level renaming (zero to 0ℓ) hiding (suc)
+
+ open import Relation.Binary.PropositionalEquality hiding (subst)
+
+ infixr 50 _`×_ _`×'_
+ infixr 30 _`+_ _`+'_
+
+In this second part, we apply a type-theoretic concept, a *universe*,
+to manipulate some structure of interest. Here, we shall look at
+inductive types.
+
+Universes were born around the same time as type theory: they were
+introduced by Martin-Löf in `Intuitionistic Type Theory`_. Their
+application to generic programming came later with `Universes for
+Generic Programs and Proofs in Dependent Type Theory`_.
+
+Following `The Gentle Art of Levitation`_, we shall:
+ - code a universe for describing inductive types
+ - show that the resulting types admit an induction principle
+ - implement a generic datatype construction: the free monad
+ - reflect the universe in itself
+
+Vision: "Whereof one cannot speak, thereof one must be silent."
+
+--------------------------------
+Descriptions
+--------------------------------
+
+In lecture 1, we asked whether we could give a "grammar" for the
+functors used to encode the signatures of algebraic effects. As
+mentioned then, signatures are essentially the same as datatype
+definitions. We shall thus decompose our model of inductive types in,
+first, the underlying functor encoding a signature and, second, a
+fixpoint of signatures.
+
+The grammar can be understood as taking the closure of all the
+operations offering/preserving a functorial structure. Namely, the
+identity and constant functors are functors. Then, the pointwise
+product of functors is itself a functor while the indexed sum and
+product of functors is itself a functor. The *code* of the universe
+translates this intuition by describing the *smallest* set closed
+under those operations::
+
+ data Desc : Set₁ where
+ `X : Desc
+ `K : Set → Desc
+ _`×_ : (D₁ D₂ : Desc) → Desc
+ _`+_ : (D₁ D₂ : Desc) → Desc
+ `Σ : (S : Set)(D : S → Desc) → Desc
+ `Π : (S : Set)(D : S → Desc) → Desc
+
+The *interpretation* gives the desired semantics::
+
+ ⟦_⟧ : Desc → Set → Set
+ ⟦ `X ⟧ X = X
+ ⟦ `K S ⟧ X = S
+ ⟦ D₁ `× D₂ ⟧ X = ⟦ D₁ ⟧ X × ⟦ D₂ ⟧ X
+ ⟦ D₁ `+ D₂ ⟧ X = ⟦ D₁ ⟧ X ⊎ ⟦ D₂ ⟧ X
+ ⟦ `Σ S T ⟧ X = Σ[ s ∈ S ] ⟦ T s ⟧ X
+ ⟦ `Π S T ⟧ X = (s : S) → ⟦ T s ⟧ X
+
+..
+ ::
+ module Exercise-compose where
+
+**Exercise (difficulty: 2)** Note that we would expect the composition
+of two functors to be a functor. Implement composition of descriptions::
+
+ _∘D_ : Desc → Desc → Desc
+ D₁ ∘D D₂ = {!!}
+
+ correctness-∘ : ∀ {X D₁ D₂} → ⟦ D₁ ∘D D₂ ⟧ X ≡ ⟦ D₁ ⟧ (⟦ D₂ ⟧ X)
+ correctness-∘ = {!!}
+ where postulate ext : Extensionality 0ℓ 0ℓ
+
+
+
+**Exercise (difficulty: 2)** We claim that our description interpret
+to functors. We ought to be able to equip *any* description with a
+functorial action::
+
+ map : ∀ {X Y} → (D : Desc)(f : X → Y)(v : ⟦ D ⟧ X) → ⟦ D ⟧ Y
+ map = {!!}
+
+and (generically) prove the functor laws::
+
+ proof-map-id : ∀ {X} → (D : Desc)(v : ⟦ D ⟧ X) → map D id v ≡ v
+ proof-map-id = {!!}
+ where postulate ext : Extensionality 0ℓ 0ℓ
+
+ proof-map-compos : ∀ {X Y Z}{f : X → Y}{g : Y → Z} →
+ (D : Desc)(v : ⟦ D ⟧ X) →
+ map D (λ x → g (f x)) v ≡ map D g (map D f v)
+ proof-map-compos = {!!}
+ where postulate ext : Extensionality 0ℓ 0ℓ
+
+
+
+--------------------------------
+Fixpoint
+--------------------------------
+
+The functors captured by our grammar have also the property of being
+"strictly-positive". We are therefore allowed to take their fixpoint::
+
+ data μ (D : Desc) : Set where
+ ⟨_⟩ : ⟦ D ⟧ (μ D) → μ D
+
+Over this (standard) inductive type, we can implement the traditional
+``fold`` operator::
+
+ {-# TERMINATING #-}
+ fold : (D : Desc){T : Set} →
+ (⟦ D ⟧ T → T) → μ D → T
+ fold D α ⟨ x ⟩ = α (map D (fold D α) x)
+
+**Exercise (difficulty: 3)** Convince the termination checker that
+``fold`` is indeed terminating. Hint: manually specialize the
+partially applied function ``map D (fold D α)`` in a definition
+mutually-recursive with ``fold``.
+
+..
+ ::
+ module Example-Nat where
+
+**Example: natural numbers**:: Natural numbers are thus described as
+follows::
+
+ data NatTag : Set where
+ `Ze `Su : NatTag
+
+ NatD : Desc
+ NatD = `Σ NatTag (λ { `Ze → `K ⊤
+ ; `Su → `X })
+
+ Nat : Set
+ Nat = μ NatD
+
+ pattern ze = ⟨ `Ze , tt ⟩
+ pattern su n = ⟨ `Su , n ⟩
+
+Using the ``fold``, we can implement addition over these numbers::
+
+ plus : Nat → Nat → Nat
+ plus x = fold NatD (λ { (`Ze , tt) → x
+ ; (`Su , rec) → su rec })
+
+ test : plus (su (su ze)) (su (su (su ze)))
+ ≡ su (su (su (su (su ze))))
+ test = refl
+
+..
+ ::
+ module Example-List where
+
+**Example: lists**:: Similarly, here are lists::
+
+ data ListTag : Set where
+ `Nil `Cons : ListTag
+
+ ListD : Set → Desc
+ ListD X = `Σ ListTag (λ { `Nil → `K ⊤
+ ; CCons → `Σ X λ _ → `X })
+
+ List : Set → Set
+ List X = μ (ListD X)
+
+ nil : ∀ {X} → List X
+ nil = ⟨ `Nil , tt ⟩
+
+ cons : ∀ {X} → X → List X → List X
+ cons x t = ⟨ `Cons , x , t ⟩
+
+**Exercise (difficulty: 1)**:: Implement binary trees using descriptions.
+
+
+--------------------------------
+Induction
+--------------------------------
+
+Introducing a ``fold`` to enable recursion over ``μ D`` is
+simple(-type)-minded. Being in type theory, we actually want a
+recursion principle. We obtain it by instantiating the usual framework
+for induction::
+
+
+ All : ∀{X} → (D : Desc)(P : X → Set) → ⟦ D ⟧ X → Set
+ All `X P x = P x
+ All (`K Z) P x = ⊤
+ All (D₁ `× D₂) P (d₁ , d₂) = All D₁ P d₁ × All D₂ P d₂
+ All (D₁ `+ D₂) P (inj₁ d₁) = All D₁ P d₁
+ All (D₁ `+ D₂) P (inj₂ d₂) = All D₂ P d₂
+ All (`Σ S T) P (s , xs) = All (T s) P xs
+ All (`Π S T) P k = ∀ s → All (T s) P (k s)
+
+ Rec-μ : ∀ D → RecStruct (μ D) _ _
+ Rec-μ D P ⟨ xs ⟩ = All D P xs
+
+ all : ∀ {X P} → (D : Desc) → (rec : (x : X) → P x)(x : ⟦ D ⟧ X) → All D P x
+ all `X rec x = rec x
+ all (`K S) rec z = tt
+ all (D₁ `× D₂) rec (d₁ , d₂) = all D₁ rec d₁ , all D₂ rec d₂
+ all (D₁ `+ D₂) rec (inj₁ d₁) = all D₁ rec d₁
+ all (D₁ `+ D₂) rec (inj₂ d₂) = all D₂ rec d₂
+ all (`Σ S T) rec (s , xs) = all (T s) rec xs
+ all (`Π S T) rec k = λ s → all (T s) rec (k s)
+
+ {-# TERMINATING #-}
+ rec-μ-builder : ∀{D} → RecursorBuilder (Rec-μ D)
+ rec-μ-builder {D} P rec ⟨ xs ⟩ = all D (λ x → rec x (rec-μ-builder P rec x)) xs
+
+ induction : (D : Desc)(P : μ D → Set) →
+ ((x : ⟦ D ⟧ (μ D)) → All D P x → P ⟨ x ⟩) →
+ (x : μ D) → P x
+ induction D P ms xs = build rec-μ-builder P (λ { ⟨ x ⟩ x₁ → ms x x₁ }) xs
+
+**Exercise (difficulty: 3)**:: Convince the termination checker that
+induction is terminating, either by implementing ``rec-μ-builder`` in
+an obviously terminating manner, or by writing ``induction`` directly
+in terms of ``all``.
+
+
+..
+ ::
+ module Example-Plus where
+ open Example-Nat hiding (plus)
+
+Using induction, we can write any dependently-typed programs or proofs
+over described inductive types: they have become (mostly, modulo the
+fact that we have to go trough the fold/induction principle, which is
+not idiomatic Agda) first-class objects.
+
+But we can also take this as a opportunity to understand what we did
+earlier, in a simply-typed setting::
+
+ plus[_∶_] : Nat → Nat → Set
+ plus[ m ∶ n ] = Nat
+
+ plus : (m n : Nat) → plus[ m ∶ n ]
+ plus m = induction NatD (λ n → plus[ m ∶ n ])
+ (λ { (`Ze , tt) tt → m
+ ; (`Su , n) rec → su rec } )
+
+--------------------------------
+Generic free monad
+--------------------------------
+
+Thinking about it, we now have first-class inductive types (modulo
+encoding, again). This means that we can craft new datatypes from
+existing datatypes. We exercise this possibility by implementing a
+generic free monad construction.
+
+In its most brutal form, the free monad construction consists in
+grafting an extra constructor containing a value of a provided type,
+the elements of the earlier signature being integrated as operations
+``op``::
+
+ _*D_ : Desc → Set → Desc
+ D *D X = `Σ Bool λ { true → `K X ; false → D }
+
+ Free : Desc → Set → Set
+ Free D X = μ (D *D X)
+
+ return : ∀ {D X} → X → Free D X
+ return x = ⟨ true , x ⟩
+
+ op : ∀ {D X} → ⟦ D ⟧ (Free D X) → Free D X
+ op xs = ⟨ false , xs ⟩
+
+Doing so, the resulting description has a monadic structure, which we
+can realize generically::
+
+ subst[_∶_∶_] : ∀ {X Y} → (D : Desc) → Free D X → (X → Free D Y) → Set
+ subst[_∶_∶_] {X}{Y} D _ _ = Free D Y
+
+ subst : ∀ {X Y} → (D : Desc) →
+ Free D X → (X → Free D Y) → Free D Y
+ subst {X}{Y} D mx k =
+ induction (D *D X) (λ mx₁ → subst[ D ∶ mx ∶ k ])
+ (λ { (true , x) tt → k x
+ ; (false , xs) as → ⟨ false , help D xs as ⟩ })
+ mx
+ where help : ∀ {X Y} D → (ds : ⟦ D ⟧ X) → All D (λ _ → Y) ds → ⟦ D ⟧ Y
+ help `X ds as = as
+ help (`K x) ds as = ds
+ help (D₁ `× D₂) (ds₁ , ds₂) (as₁ , as₂) = help D₁ ds₁ as₁ , help D₂ ds₂ as₂
+ help (D₁ `+ D₂) (inj₁ ds₁) as₁ = inj₁ (help D₁ ds₁ as₁)
+ help (D₁ `+ D₂) (inj₂ ds₂) as₂ = inj₂ (help D₂ ds₂ as₂)
+ help (`Σ S D₁) (s , ds) as = s , help (D₁ s) ds as
+ help (`Π S D₁) ds as = λ s → help (D₁ s) (ds s) (as s)
+
+..
+ ::
+ module Example-Free (A : Set)(B : A → Set) where
+
+ CallD : Desc
+ CallD = `Σ A λ a → `Π (B a) λ _ → `X
+
+ RecMon : Set → Set
+ RecMon = Free CallD
+
+ call : ∀ {X} → (a : A)(rec : B a → RecMon X) → RecMon X
+ call a rec = op (a , rec)
+
+ substR : ∀ {X Y} → RecMon X → (X → RecMon Y) → RecMon Y
+ substR = subst CallD
+
+ test : ∀ {a₁ a₂ a₃} →
+ (substR (call a₁ return)
+ (λ ba₁ → call a₂ (λ ba₂ → call a₃ return)))
+ ≡ (call a₁ λ ba₁ → call a₂ (λ ba₂ → call a₃ return))
+ test = refl
+
+**Exercise (difficulty: 4)**:: Prove the monad laws.
+
+
+--------------------------------
+Bootstrap
+--------------------------------
+
+So far, we have been doing "generic programming" on the one hand
+(computing over Desc) and "programming" on the other hand (computing
+over anything else, including inhabitants of ``μ D``, for ``D :
+Desc``). This may have gone unnoticed (probably because doing anything
+with these encodings is blindly painful) but, in a standalone
+language, this would mean having two "programming languages" in the
+programming language, one for generic programming and the other for
+programming.
+
+There may be two solutions to this problem: either we (pragmatically)
+make the generic programming language to borrow as much as possible
+from the programming language, or we (brutally) collapse the
+programming language into the generic programming language. For
+obvious reasons (having to do with full employment), we chose the
+latter. The key idea consists in noticing that ``Desc`` itself is an
+inductive type. As such, it can be described::
+
+ DescD : Desc
+ DescD = `K ⊤
+ `+ `K Set
+ `+ (`X `× `X)
+ `+ (`X `× `X)
+ `+ (`Σ Set λ S → `Π S (λ _ → `X))
+ `+ (`Σ Set λ S → `Π S (λ _ → `X))
+
+ Desc' : Set₁
+ Desc' = μ DescD
+
+ `X' : Desc'
+ `X' = ⟨ inj₁ tt ⟩
+
+ `K' : Set → Desc'
+ `K' S = ⟨ inj₂ (inj₁ S) ⟩
+
+ _`×'_ : Desc' → Desc' → Desc'
+ D₁ `×' D₂ = ⟨ inj₂ (inj₂ (inj₁ (D₁ , D₂) )) ⟩
+
+ _`+'_ : Desc' → Desc' → Desc'
+ D₁ `+' D₂ = ⟨ inj₂ (inj₂ (inj₂ (inj₁ (D₁ , D₂) ))) ⟩
+
+ `Σ' : (S : Set)(T : S → Desc') → Desc'
+ `Σ' S T = ⟨ inj₂ (inj₂ (inj₂ (inj₂ (inj₁ (S , T))))) ⟩
+
+ `Π' : (S : Set)(T : S → Desc') → Desc'
+ `Π' S T = ⟨ inj₂ (inj₂ (inj₂ (inj₂ (inj₂ (S , T))))) ⟩
+
+Note that, aside from the constructor ``⟨_⟩`` of ``μ``, the
+constructor of ``Desc'`` only depend on constructors pre-existing in
+the type theory (unit, cartesian product, injections into sum): in an
+implementation, we can simply take these codes as the *definition*. We
+then only need to implement the fixpoint operator and its induction
+principle: this provides us with the ability to compute over inductive
+types on one hand (programming) but also, in particular, to compute
+over Desc since it is described in itself (generic programming).
+
+************************************************
+Conclusion
+************************************************
+
+We have seen two complementary approaches to generic programming. In
+both cases, we have exploited (type-class) or built (universe) a
+mechanism that allows us to reify a subset of the programming language
+in itself.
+
+Whichever mechanism we chose depends highly on the functionalities
+offered by the programming language. For instance, Coq type-classes
+are extremely powerful whereas its strict-positive criteria is
+extremely obtuse: as a result, the extensional approach works well
+whereas the intensional one is nearly impossible.
+
+**Exercises (difficulty: open ended):**
+ - Implement Section 6 to 8 of Gibbons' paper (in Coq, probably)
+ - Extend ``Desc`` to encode inductive families
+ - Extend ``Desc`` to support internal fixpoints (such as ``data Rose A = rose : List (Rose A) → Rose A``)
+
+**Going further, extensionally:**
+ - Other examples of `functor-oriented programming `_: `unification-fd `_, `lenses `_
+ - Structures in idiomatic Agda: `Agda Prelude`_
+
+
+
+
+
+.. References (papers):
+.. _`APLicative Programming Naperian Functors`: https://doi.org/10.1007/978-3-662-54434-1_21
+.. _`An agda formalisation of the transitive closure of block matrices`: https://doi.org/10.1145/2976022.2976025
+.. _`Intuitionistic Type Theory`: https://www.worldcat.org/search?q=isbn%3A8870881059
+.. _`Universes for Generic Programs and Proofs in Dependent Type Theory`: http://www.cse.chalmers.se/~patrikj/poly/gendt/
+.. _`The Gentle Art of Levitation`: https://doi.org/10.1145/1863543.1863547
+
+.. References (online):
+.. _`Typeclassopedia`: https://wiki.haskell.org/Typeclassopedia
+.. _`representable functor`: https://ncatlab.org/nlab/show/representable+functor
+.. _`Agda prelude`: https://github.com/UlfNorell/agda-prelude
+
+.. Local Variables:
+.. mode: agda2
+.. End:
+
diff --git a/agda/Index.lagda.rst b/agda/Index.lagda.rst
index bd7848bba70cc616bd8631544c35a024098d73d1..f753f37a0a555b34641d9475e4594ca0b171d777 100644
--- a/agda/Index.lagda.rst
+++ b/agda/Index.lagda.rst
@@ -11,6 +11,7 @@ MPRI 2.4 : Dependently-typed Functional Programming
open import 01-effectful.Monad
open import 02-dependent.Indexed
open import 03-total.Recursion
+ open import 04-generic.Desc
************************************************
diff --git a/slides/pedagand-04.pdf b/slides/pedagand-04.pdf
new file mode 100644
index 0000000000000000000000000000000000000000..3d39c49c506cfb44455b7b45c9b282b7937ae4a0
Binary files /dev/null and b/slides/pedagand-04.pdf differ