# 2020-01-22 `FinVec2`: Modified the types of some functions

```
module FinVec2 where

open import Level using (Level) renaming ( _⊔_ to _⊍_ )
open import Data.Product as Product using ( _×_ ; _,_ ; Σ ; proj₁ ; proj₂ )
open import Data.Nat using ( ℕ ; zero ; suc ; _<_ ; z≤n ; s≤s )

open import Function using ( _∘′_ ; id )

open import Relation.Binary.PropositionalEquality using ( _≡_ ; _≗_ ; refl ; cong ; module ≡-Reasoning )
```

Note that we import `_∘′_` instead of `_∘_`, since we do not need to compose functions of dependent function types in this module,
and restricting composition to functions of non-dependent types makes type inference easier and frequently more helpful.

A pretty syntax for dependent sum types, that is, types of dependently-typed pairs:
```
Σ-syntax : {ℓa ℓb : Level} (A : Set ℓa) (B : A → Set ℓb) → Set (ℓa ⊍ ℓb)
Σ-syntax = Σ

infix 2 Σ-syntax
syntax Σ-syntax A (λ a → B) = Σ a ∶ A • B
```
In a `syntax` declaration, the right-hand side is the new syntax that is introduced,
and the left-hand side is what it is expanded to.


## Prototypical Finite Types: `Fin`

The type `Fin n` can be seen as an inductive implementation
of the set of all natural numbers less than `n`.
Informally:

  Fin 0 = {}
  Fin 1 = { 0 }
  Fin 2 = { 0 , 1 }

```
data Fin : ℕ → Set where
  zero : {n : ℕ} → Fin (suc n)
  suc : {n : ℕ} → Fin n → Fin (suc n)
```

  suc (zero : Fin 1) : Fin 2

```
toℕ : {n : ℕ} → Fin n → ℕ
toℕ zero = 0
toℕ (suc i) = suc (toℕ i)
```

For each `n`, the function `toℕ {n}` is injective:
```
suc-injective : {m n : ℕ} → ℕ.suc m ≡ suc n → m ≡ n
suc-injective = ?

toℕ-injective : {n : ℕ} {i j : Fin n} → toℕ i ≡ toℕ j → i ≡ j
toℕ-injective = ?
```

But since `toℕ {n}` is not surjective, we cannot define a full inverse:

  fromℕ : {n : ℕ} → (m : ℕ) → Fin n -- cannot be injective because of pigeon-hole

  toℕ-fromℕ : {n : ℕ} (m : ℕ) → toℕ (fromℕ m) ≡ m   -- cannot be made to hold

Since the range of the function `toℕ {n}` contains exactly the
natural numbers that are smaller than `n`,
the restriction to these makes it possible to define an inverse function for `toℕ {n}`:
```
fromℕ′ : {n : ℕ} → (Σ m ∶ ℕ • m < n) → Fin n
fromℕ′ (zero , s≤s m<n) = zero
fromℕ′ (suc m , s≤s m<n) = suc (fromℕ′ (m , m<n))
```

```
toℕ-bound : {n : ℕ} (i : Fin n) → toℕ i < n
toℕ-bound = ?

toℕ′ : {n : ℕ} → Fin n → (Σ m ∶ ℕ • m < n)
toℕ′ i = toℕ i , toℕ-bound i
```

If we defined this correctly,
we can now easily show the first inverse property:
```
fromℕ-toℕ : {n : ℕ} → fromℕ′ {n} ∘′ toℕ′ {n} ≗ id
-- Note that due to the definition of `_≗_`, this is the same as:
-- fromℕ-toℕ : {n : ℕ} (i : Fin n) → fromℕ′ (toℕ′ i) ≡ i
fromℕ-toℕ = ?
```

*Big Challenge*:
It is actually possible to show also the second inverse property.
(Why is it non-obvious that this is possible?
Can you formalise the underlying property?)
```
toℕ-fromℕ : {n : ℕ} → toℕ′ {n} ∘′ fromℕ′ {n} ≗ id
-- Note that due to the definition of `_≗_`, this is the same as:
-- toℕ-fromℕ : {n : ℕ} (p : Σ m ∶ ℕ • m < n) → toℕ′ (fromℕ′ p) ≡ p
toℕ-fromℕ = ?
```

## Known-length “Vectors”

An element of the type `Vec A n` is a vector of `n` elements of type `A`.

```
infixr 5 _∷_
data Vec (A : Set) : ℕ → Set where
  [] : Vec A zero
  _∷_ : A → {n :  ℕ} → Vec A n → Vec A (suc n)
```

```
_!_ : {A : Set} {n : ℕ} → Vec A n → (Fin n → A)
(x ∷ xs) ! zero = x
(x ∷ xs) ! suc i = xs ! i
```

The parentheses in the type of `_!_` emphasis that we can
think of `_!_ {A} {n}` as a function
that turns vectors of type `Vec A n`
into functions of type `Fin n → A`.
This has an inverse:

```
tabulate : {A : Set} {n : ℕ} → (Fin n → A) → Vec A n
tabulate {n = zero} f = []
tabulate {n = suc n} f = (f zero) ∷ (tabulate (f ∘′ suc))
```

If we defined this correctly, we can prove the inverse properties.
(Note that `C-u C-u` before `C-c C-,`, respectively before `M-x agda2-goal-and-context`,
simplifies the reported types)
You may want to expand `_≗_` again so that you see more clearly how to continue:

```
tabulate-! : {A : Set} {n : ℕ} → tabulate {A} {n} ∘′ _!_ ≗ id
tabulate-! = {!!}

!-tabulate : {A : Set} {n : ℕ} → (f : Fin n → A) → _!_ (tabulate f) ≗ f
!-tabulate = {!!}
```

The above `!-tabulate` is actually not in the canonic shape of an inverse property.
Try on |!-tabulate′| how far you can get with that shape:

```
!-tabulate′ : {A : Set} {n : ℕ} → _!_ ∘′ tabulate {A} {n} ≗ id
!-tabulate′ f = {!!}
```

Something easy at the end: Map a function over a vector:

```
vmap : {A B : Set} → (A → B) → {n : ℕ} → Vec A n → Vec B n
vmap = {!!}
```
Test case for |vmap|:
```
vmap-test₁ : vmap suc (3 ∷ 5 ∷ []) ≡ 4 ∷ 6 ∷ []
vmap-test₁ = {! refl !}
```
`vmap` distributes over function composition:
```
vmap-∘ : {A B C : Set} (f : A → B) (g : B → C) {n : ℕ} → vmap (g ∘′ f) {n} ≗ vmap g ∘′ vmap f
vmap-∘ = {!!}
```


Zip two equal-length vectors together:
```
zip : {A B : Set} {n : ℕ} → Vec A n → Vec B n → Vec (A × B) n
zip = {!!}
```

```
proj₁-zip : {A B : Set} {n : ℕ} (xs : Vec A n) (ys : Vec B n) → vec-map proj₁ (zip xs ys) ≡ xs
proj₁-zip = {!!}
```