Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
M
mpri-2.4-public
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
0
Issues
0
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
Packages
Packages
Container Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
POTTIER Francois
mpri-2.4-public
Commits
c234254b
Commit
c234254b
authored
Feb 15, 2018
by
Pierre-Évariste Dagand
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Lecture 4 goes live
parent
c077ad80
Changes
4
Show whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
1640 additions
and
1 deletion
+1640
-1
README.md
README.md
+1
-1
Desc.lagda.rst
agda/04-generic/Desc.lagda.rst
+1638
-0
Index.lagda.rst
agda/Index.lagda.rst
+1
-0
pedagand-04.pdf
slides/pedagand-04.pdf
+0
-0
No files found.
README.md
View file @
c234254b
...
...
@@ -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
...
...
agda/04-generic/Desc.lagda.rst
0 → 100644
View file @
c234254b
..
::
{-# 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 <https://doi.org/10.1145/1863543.1863547>`_
- 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 <https://wiki.haskell.org/Typeclassopedia#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 <https://wiki.haskell.org/Typeclassopedia#Applicative>`_::
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 <https://stackoverflow.com/questions/12963733/writing-cojoin-or-cobind-for-n-dimensional-grid-type/13100857#13100857>`_
**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
<https://wiki.haskell.org/Typeclassopedia#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 <https://doi.org/10.1145/2699681>`_), 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
<https://wiki.haskell.org/Typeclassopedia#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::