{%hackmd @YuRen-tw/article-theme %}

# 談 Void：以依值型態語言 Idris 為例

在許多程式語言中，我們可以為變數或函式標上型態。
型態能用來提示這個東西的結構以及它如何被使用，比如整數型態能做整數運算。
在實際執行程式以前，機器可以以此決定要分配多少空間來容納資料，或是根據型態做出特定的最佳化。
同時我們也能先透過型態檢查來避免人類的編寫錯誤，比如錯誤地將整數與文字相減。
更進一步地，我們也發展了型態理論（type theory），研究一個型態系統究竟可以表達出哪些機制來輔助我們。

這篇討論我們會提到兩種特別的型態：`Unit` 與 `Void`。

<div class="definition unnumbered" data-info="Unit 與 Void">

- 只有一個值屬於 `Unit` 型態，那個值記為 `()`。
- 沒有任何值屬於 `Void` 型態。
</div>

它們在某些程式語言中可能有不同的稱呼，但任何滿足定義的我們在這篇都統一用 `Unit` 與 `Void` 稱呼。
有些人可能會覺得這兩種型態很類似，但它們在型態系統中究竟有什麼差異？

我們在這篇文會先從理論的方面介紹 `Unit` 與 `Void`，再利用依值型態語言 Idris 的實際例子體會 `Void` 在系統中的功用。
最後的實際例子參考了 Stack Overflow 問題 [What's the absurd function in Data.Void useful for?](https://stackoverflow.com/questions/14131856/whats-the-absurd-function-in-data-void-useful-for) 的其中一則回答。

## `Unit` 與 `Void`

整數型態有 `-1`、`0`、`1`、`2` 等等的數值，而布林型態也有 `True` 與 `False` 這兩個值，它們都透過不同的運算行為來代表不同的意義。
單純從定義來看，沒有任何值的 `Void` 型態似乎沒有意義。
而 `Unit` 型態只有一個值，型態內不存在其他值能與它區別，這個值也就不帶有任何意義。
用集合的角度來看，`Void` 就像是空集合，而 `Unit` 是只裝有空集合的集合，看起來這兩種型態都相當無用。
它們究竟有什麼差別？
它們在型態系統中到底又扮演著什麼角色呢？

在理論的這一面，我們有「Curry--Howard 對應」，它告訴我們程式語言、邏輯、數學的範疇論（category）這三個看似各自獨立的領域之間其實有一個緊密的對應關係，那些看似完全不同的概念事實上指的是同樣的存在。

<div class="theorem unnumbered" data-name="酷理論" data-info="Curry&ndash;Howard 對應（簡略版）">

| 程式 | 範疇 | 邏輯 |
| :---: | :---: | :---: |
| 型態 | 物件 | 命題 |
| 函式 | 態射 | 蘊含，$\to$ |
| `Unit` | 終物件，$1$ | 真，$\top$ |
| `Void` | 始物件，$0$ | 假，$\bot$ |
| 和型態 | 餘積 | 析取，$\vee$ |
| 積型態 | 積 | 合取，$\wedge$ |
</div>

從上面簡略的對應表可以看出，`Unit` 跟 `Void` 其實是互相對偶的存在。
我們也能從它們在範疇與邏輯這兩個平行宇宙中擔任的角色，來感受它們在程式語言中的意義。

### 從範疇的角度來看

範疇論研究物件與態射，用抽象而普適的語言為給各個數學領域提供一個共通的背景架構。
在這裡，我們可以將程式語言的所有型態考慮為範疇中的物件，函式則視為物件之間的態射。
那麼對於這個「型態範疇」，只有單個值 `()` 的 `Unit` 型態便是範疇中的終物件，而沒有任何值的 `Void` 型態則是範疇中的始物件。

在範疇論中，我們關心的焦點並不是物件內部的性質，而是物件與物件之間如何利用態射互相關聯。
所以我們通常會透過這些物件之間的關聯來定義物件在範疇中所擔任的角色，這些關聯也被稱作泛性質（universal property）。

<div class="definition unnumbered" data-info="終物件與始物件">

- 範疇中的終物件如果存在，則記為 $1$。它定義為滿足以下泛性質的物件：
- 對於範疇中的任意物件 $X$ 都存在唯一的態射 $X \to 1$。
- 範疇中的始物件如果存在，則記為 $0$。它定義為滿足以下泛性質的物件：
- 對於範疇中的任意物件 $X$ 都存在唯一的態射 $0 \to X$。
</div>

我們可以看到對於任意型態 `t`，的確都能定義函式

f : t -> Unit
f x = ()

而且上面的函式 `f` 的確會是唯一的，很明顯因為 `Unit` 只有唯一的值 `()`，我們只能這樣定義函式。
另一方面，就算有多個 `Unit` 型態，它們其實也會互相同構，也就是說它們在型態系統中的功能完全可以互相取代。

程式語言中 `Unit` 型態的例子有 Rust 的 `()`、Python 的 `NoneType`、JavaScript 的 `null` 與 `undefined`（沒錯，JavaScript 有兩個 `Unit` 型態）。
我們提及這些東西時常常不區分談論的是型態還是它的值本身，因為型態裡只有一個值。
不過我們也會發現，所謂函式唯一或型態同構的性質其實並不太適用於上述幾個容許副作用的程式語言。
比如 Python 的函式 `print` 與 `exec` 都可以視為有型態 `str -> NoneType`，但它們的功能卻不相同。
這是因為這類函式真正的功能是執行時的副作用，而 `Unit` 型態大多只是為了讓型態系統更加好用而拿來表示「空的參數值」或「空的回傳值」的一個符號而已。

如何把副作用包裝好使得它不破壞型態系統原本應該擁有的好性質，是個複雜的議題，我們沒辦法在這篇文裡面討論。
在後續的篇章裡面我們就姑且忘了副作用這件事吧。

作為與 `Unit` 型態對偶的 `Void` 型態也有相同的函式唯一性或型態同構性。
但當我們想為任意型態 `t` 定義那個 `Void -> t` 的函式時，可能會發現無從下手，因為 `Void` 型態裡根本沒有值讓我們定義對應關係。
而事實上這正是這個函式的定義法：什麼對應都沒有。
於是當這種函式被定義出來時就自然會是唯一的，因為若 `f` 跟 `g` 都是 `Void -> t` 的函式，我們找不到任何 `Void` 型態的值 `x` 代入兩者後會有所不同，因為 `Void` 型態就是沒有值。

這看起來有點詭異，但我們在最後會看到這個概念如何在程式語言中發揮作用。

### 從邏輯的角度來看

換個角度，我們也能將型態視為邏輯裡的命題、將函式視為邏輯裡的蘊含（implication），那麼型態的值就相當於命題的證明了。

有一點要特別注意：我們這時所談的「命題為真」是指命題的證明有辦法被構造出來。
這跟討論命題的真值是有所差別的，因為反駁命題的證明無法被構造出來並不代表支持命題的證明就有方法被構造，也就是說命題並不總是非假即真。
排中律既然不存在，我們就不能訴諸真值表。

我們在這裡會用「$\Gamma \vdash P$」這段語句來代表「假設有 $\Gamma$ 的證明時，就能構造出命題 $P$ 的證明」，其中 $\Gamma$ 可以有複數個命題，也可以沒有命題。
對應到程式語言，相當於說「假設有型態 $\Gamma$ 的一些值，就能構造出型態 $P$ 的值」。
而「$\Gamma \vdash P$」也不能憑空亂寫，邏輯系統中都會設定數個推論規則來從一些的語句「推論」出其他語句。
最基本通常都會有一條推論規則：如果 $\Gamma$ 中有命題 $P$，則必定有「$\Gamma \vdash P$」。
這些規則告訴我們該如何構造證明，以及如何被用來構造其他證明，換句話說也形塑了命題在邏輯系統裡的意義。

我們先看對應於程式語言中函式 `P -> Q` 的蘊含「$P \to Q$」，透過以下的推論規則，在邏輯系統中它有「若 $P$ 則 $Q$」的意義。

<div class="definition unnumbered" data-name="推論規則" data-info="蘊含">

- 【蘊含引入】當有 $\Gamma, P \vdash Q$，就有 $\Gamma \vdash P \to Q$。
- 【蘊含消去】當有 $\Gamma \vdash P \to Q$ 與 $\Gamma \vdash P$，就有 $\Gamma \vdash Q$。
</div>

上面規則中的 $\Gamma$ 只是代表其他可能既有的多個命題。
我們可以看到，【蘊含引入】相當於定義函式：當得到型態 `P` 的參數後能構造出型態 `Q` 的值來回傳，就能定義出 `P -> Q` 的函式。
而【蘊含消去】則相當於使用函式：若有函式 `f : P -> Q` 與型態 `P` 的值 `x`，那麼將 `x` 作為引數代入後的回傳值 `f x` 就屬於型態 `Q`。

在這樣的系統裡，只有單個值 `()` 的 `Unit` 型態就是必定有證明的「$\top$，真，恆真式」，而沒有任何值的 `Void` 型態則是不允許被證明的「$\bot$，假，矛盾式」。

<div class="definition unnumbered" data-name="推論規則" data-info="真與假">

- 【$\top$ 引入】對任意的 $\Gamma$，都有 $\Gamma \vdash \top$。
- 【$\bot$ 消去】對任意命題 $P$，都有 $\bot \vdash P$。
</div>

上述的推論規則如果套用了【蘊含引入】，就可以得到以下結論：

<div class="definition unnumbered" data-name="性質" data-info="真與假">

- 對任意命題 $P$ 都能證明出 $P \to \top$。
- 【爆炸原理】對任意命題 $P$ 都能證明出 $\bot \to P$。
</div>

根據【蘊含消去】，【爆炸原理】就代表說「若能證明出矛盾，則能證明出任何命題」。
這雖然聽起來很奇怪，但它讓我們在邏輯系統中有辦法處理一些不可能發生卻需要被證明的命題。
例如在處理析取（disjunction）命題「$P \vee Q$」的時候。

<div class="theorem unnumbered" data-name="推論規則" data-info="析取">

- 【析取引入左】當有 $\Gamma \vdash P$，就有 $\Gamma \vdash P \vee Q$。
- 【析取引入右】當有 $\Gamma \vdash Q$，就有 $\Gamma \vdash P \vee Q$。
- 【析取消去】當有 $\Gamma \vdash P \vee Q$ 與 $\Gamma, P \vdash R$ 與 $\Gamma, Q \vdash R$，就有 $\Gamma \vdash R$。
</div>

這些規則為析取命題 $P\vee Q$ 形塑了「$P$ 或 $Q$」的意義。
其中【析取消去】代表前提 $\Gamma$ 若能證明出有 $P$ 或 $Q$，而且無論再多假設 $P$ 或 $Q$ 都能殊途同歸證明出 $R$，那麼前提 $\Gamma$ 就能證明出 $R$。
但若在那個前提下 $P$ 根本不會發生，也就是多了 $P$ 就會產生矛盾時，我們就能利用【爆炸原理】完成「$\Gamma, P \vdash R$」的工作。

邏輯中，我們也可以將任意命題 $P$ 的否命題 $\neg P$ 定義為 $P \to \bot$，意即「若能證明 $P$ 則會證明出矛盾」。
於是對任意命題 $P$ 與 $Q$，【爆炸原理】也可以被描述為 $(P \wedge \neg P) \to Q$。

類似地，我們能在程式語言中利用 `Void` 以及相當於【爆炸原理】的函式 `Void -> t`（對任意型態 `t`），定義出型態安全的完全函數，而不會遺漏任何情形，就算我們明確知道某些情形實際上根本不會發生。
我們接下來將透過程式語言 Idris 的實際例子來體驗這個機制的奧妙之處。
而在實際看這個例子以前，我們必須先稍微認識一下什麼是 Idris。

## Idris 背景知識

Idris 是一個有依值型態的函式型程式語言，語法風格類似於 Haskell。

在 Haskell 中，我們使用 `[a]` 來代表元素屬於型態 `a` 的列表型態。
這裡的小寫 `a` 是一個型態變數，而型態 `[a]` 則「依賴」於型態 `a`：當我們在某處確定了 `a` 的實際型態，那麼就確定了 `[a]` 的實際型態。

這是一種達成泛型（generic）的方式。
比如想定義一個函式 `singleton` 將參數包成單元素列表回傳，也就是說 `singleton 13` 會是 `[13]`，那麼這樣的函式會有型態 `Int -> [Int]`。
但很明顯這個定義不必侷限在整數型態上，我們希望它可以同時應用於其他型態，而不需要為了各個型態再定義一個行為相同的函式。
於是我們可以將這個函式的型態改寫成 `a -> [a]`，而 Haskell 就會透過代入的引數型態來確定 `a` 的型態，進而確定整個 `singleton` 函式的型態。

所謂依值型態的表達力則更加強大，它代表說型態不只可以依賴於另一個型態，甚至能依賴於某個值。
比如在 Idris 中能使用 `Vect n a` 用來代表長度為 `n` 且元素屬於 `a` 型態的列表型態，這裡的變數 `a` 同樣代表型態，但變數 `n` 卻是一個屬於自然數型態 `Nat` 的值！

### 代表自然數的 `Nat` 型態

`Nat` 型態代表自然數，一個自然數要不是 $0$，要不就是某個自然數 $n$ 的後繼數 $S(n)$，或者說 $n + 1$。
這種「要不是…，要不就是…」的形式正是邏輯中的析取命題的意義，而析取命題對應到程式型態系統中就是和型態（sum type）。

在 Idris 中，是 `Nat` 型態正是以和型態的形式來定義：

data Nat : Type
  Z : Nat
  S : Nat -> Nat

上面的程式碼定義了 `Nat` 型態，它代表 `Nat` 型態有兩種建構值的方式：一種是直接用代表自然數 $0$ 的值 `Z`；一種是透過代表後繼函數 $S$ 的函式 `S`，將某個屬於 `Nat` 型態的值 `n` 作為引數代入後回傳得到屬於 `Nat` 型態的值 `S n`。

> 為了方便使用，Idris 提供了一些語法糖：
> - `0` 代表 `Z`
> - `1` 代表 `S Z`
> - `5` 代表 `S (S (S (S (S Z))))`

就如同先前提過的【析取消去】，當我們能由前提證明出析取命題 $P \vee Q$，必須要再說各別假設 $P$ 或 $Q$ 之後都能殊途同歸證明出 $R$，才能推論說我們的前提能證明 $R$。
在程式語言中，若要處理和型態的值，則通常會透過模式比對（pattern matching）來各別處理不同方式建構出的值。

例如，要定義「輸入的自然數是否為零」的函式 `isZero : Nat -> Bool`，我們的參數會是以和型態定義的 `Nat`，於是我們就要分別為不同的模式 `Z` 與 `S n` 定義對應的布林值。

isZero : Nat -> Bool
isZero Z     = True
isZero (S n) = False

### 在型態裡記錄長度的 `Vect` 型態

之前說到紀錄長度的 `Vect` 型態也是以類似的方式定義：

data Vect : Nat -> Type -> Type where
  Nil  : Vect Z a
  (::) : a -> Vect n a -> Vect (S n) a

我們可以把 `Vect` 看成接受一個屬於 `Nat` 的值與一個型態，並回傳我們所需列表型態的特殊函式。
所以事實上，`Vect` 型態是一堆型態的集合體，透過代入不同的值與型態引數，可以得到某個特定的列表型態。

這同樣是以和型態的形式定義的，所以說我們定義了兩種建構方式，分別對應兩類型態：
- 長度為 `Z` 且元素屬於型態 `a` 的列表型態 `Vect Z a`
- 值只有 `Nil`，代表空的列表
- 長度為 `S n` 且元素屬於型態 `a` 的列表型態 `Vect (S n) a`
- 值有各種 `x :: xs`，代表一個元素 `x` 接上一個列表 `xs`
- 其中 `x` 屬於型態 `a`，而 `xs` 則屬於型態 `Vect n a`
- 定義裡的括號 `(::)` 代表它是中綴表示的運算子，所以值才寫成 `x :: xs`

> 為了方便使用，Idris 當然也提供了下面兩種語法糖：
> - `[]` 代表 `Nil`，屬於某個型態 `Vect 0 a`
> - `[1, 2, 3]` 代表 `1 :: 2 :: 3 :: Nil`，屬於 `Vect 3 Nat` 型態

如此一來，我們就能定義型態安全且完全的「取第一個元素」函式，而不用考慮輸入的參數會不會是空列表：

head : Vect (S n) a -> a
head (x :: xs) = x

如果我們錯誤地把空列表 `Nil` 作為引數代入 `head`，Idris 的型態系統在檢查型態時就會報告有型態錯誤，因為 `Nil` 屬於型態 `Vect Z a`，不是函式要求的型態 `Vect (S n) a`。
而如果我們把 `[1, 2, 3]` 作為引數代入 `head`，那麼 `head` 的型態就會被確定為實際的 `Vect 3 Nat -> Nat`。

### 能當作證明的 `Elem` 型態

在 Idris 中，我們能透過依值型態定義出一些意義上相當於命題的型態，這能夠用來表達或限制參數的性質。
當我們構造出了這個型態的值，也相當於建構了對應命題的一個證明。
比如我們用 `Elem` 型態當作代表命題「列表裡存在某個元素」的型態：

data Elem : a -> Vect n a -> Type where
  Here  : Elem x (x::xs)
  There : Elem x ys -> Elem x (y::ys)

我們可以把 `Elem` 看成接受一個屬於型態 `a` 的值與一個屬於型態 `Vect n a` 的列表值，並回傳「命題」的特殊函式。
同樣地，`Elem` 型態是一堆型態的集合體，代入值之後可以得到我們所需的特定「命題」。

所以我們用和型態的形式定義了兩種「推論規則」，分別對應兩類「命題」：
- 代表「`x` 元素就在第一項」的型態 `Elem x (x::xs)`
- 值有 `Here`，代表元素就在第一個
- 注意到型態裡的 `x` 與 `(x :: xs)` 重複了 `x`
- 代表「`x` 元素就在後面」的型態 `Elem x (y::ys)`
- 值有 `There p`
- 其中的 `p` 屬於 `Elem x ys` 型態
- 如果有個 `x` 在 `ys` 內的證明 `p`，就有 `x` 在 `(y :: ys)` 內的證明 `There p`

> 所以我們可以有以下的事情：
> - 「命題」`Elem 3 [3, 4]` 只有「證明」`Here`
> - 「命題」`Elem 3 [2, 3, 4]` 只有「證明」`There Here`
> - 「命題」`Elem 3 [1, 2, 3, 4]` 只有「證明」`There (There Here)`
> - 「命題」`Elem 0 [0, 0]` 有「證明」`Here` 跟 `There Here`

這時我們會發現無論用哪種規則產生出的類型中，第二個參數都是用 `(::)` 產生的列表值，也就是說漏掉了型態 `Elem x []`。
換句話說，型態 `Elem x []` 的值不存在任何建構方式。
在邏輯上這很自然，因為它代表命題「空列表裡存在某個元素」，而這無法被證明。

型態 `Elem x []` 的值不存在任何建構方式，代表它是沒有值的型態，按照我們一開始的定義，它就是一個 `Void`。
在 Idris 中，我們會為 `Elem x []` 實現 `Uninhabited` 介面。
這帶我們進入了 `Void` 的世界。

## Idris 的 `Void` 與 `Uninhabited`

我們先來看 Idris 如何定義 `Void` 型態本尊：

data Void : Type where

沒錯，沒有值，什麼都沒有。
而前面提到相當於【爆炸原理】的函式則是這樣定義：

void : (0 x : Void) -> a

一樣什麼都沒有，畢竟不可能有輸入值。
（我們先無視 `Void` 前面的 `0 x` 是什麼意思，它不影響這篇文要討論的東西）

前面也提到，沒有值的 `Void` 型態有可能不唯一，但它們都會是同構的，簡單來說都是 `Void` 的分身。
像是上一節定義 `Elem` 時，我們發現命題「空列表存在某個元素」不可能有證明，也就是說 `Elem x []` 是一個沒有值的型態。
於是 Idris 就使用 `Uninhabited` 這個介面來描述「沒有值的型態」，或者也能說是「`Void` 的分身」。

> 介面（interface）相當於 Haskell 的型態類（typeclass）或 Rust 的特徵（trait），它規範了一組可被重載的函式。
> 要讓一個型態成為某個介面的實例，我們必須實現該介面規範的某些函式。
> 然後，我們就能以定義在介面內的統一名稱呼叫實例型態的對應函式。

既然是用來描述「`Void` 的分身」，代表實現這個介面的型態都會有個函式將它與 `Void` 的值一一對應。
所以 `Uninhabited` 介面的定義如下：

interface Uninhabited t where
  uninhabited : t -> Void

這段程式碼表示說任何要實現 `Uninhabited` 介面的型態 `t` 都必須實作 `uninhabited` 函式將值映射到 `Void`。
當然，這包含 `Void` 本尊：

Uninhabited Void where
  uninhabited = id

> `id` 代表單位函式（identity，恆等函式），定義為 `id x = x`。

同樣地，`Elem x []` 也實現了 `Uninhabited` 介面：

Uninhabited (Elem x []) where
  uninhabited Here impossible

> 在 Idris 中，我們必須明確給出一個不屬於型態 `Elem x []` 的值比如 `Here`，並配上關鍵字 `impossible`，Idris 才有辦法檢測到型態 `Elem x []` 的確無法被建構。
> 這是 Idris 機制的設計。
> （參考自 Stack Overflow 的問題 [Impossible patterns in Idris](https://stackoverflow.com/questions/32947534/impossible-patterns-in-idris)）

這些 `Void` 分身在有了 `uninhabited` 函式之後就都能映射到 `Void` 本尊，然後也就有適用於這些分身的【爆炸原理】`absurd`：

absurd : Uninhabited t => t -> a
absurd h = void (uninhabited h)

上面的程式碼中 `absurd` 的型態告訴我們它能把型態 `t` 的值變成任意型態 `a` 的值，前半段的 `Uninhabited t =>` 則表示函式這個型態 `t` 必須要是 `Uninhabited` 介面的實例。

如果給了 `absurd` 某個不可能存在並屬於型態 `t` 的值 `h`，那就會先透過 `uninhabited` 變成不可能存在並屬於 `Void` 型態的值，再透過 `void` 變成任何型態 `a`的值。
但當然這實際上都不會發生，不過整件事情的型態都是完整的。

說了這麼多都還只是表達它們都是 `Void`，都有【爆炸原理】而已。
而這又有什麼用處呢？

## 利用 `Void` 的實際例子

現在我們終於來到一開始說要介紹的例子了，這個例子參考自 Stack Overflow 的問題 [What's the absurd function in Data.Void useful for?](https://stackoverflow.com/questions/14131856/whats-the-absurd-function-in-data-void-useful-for) 的其中一則回答。

在之前的介紹中，我們已經知道依值類型表達力的強大之處。
除了能把列表的長度資訊放入類型之外，還能用類型來表達一個需要被證明的命題。

接下來我們將要定義一個函式 `shrink`，我們給它一個列表 `xs`，再給它某一個元素在列表裡的「證明」`p`，最後將移除掉那一個元素後的列表回傳出來。
而且，我們希望能像之前提到的型態安全 `head` 函式一樣，在型態檢查時排除掉一些錯誤，比如對空列表裡移除元素，或是移除不在列表裡的元素。
無論我們是不小心寫錯，或是刻意欺騙，都會被型態系統擋下來。

shrink xs p = ?result

> 問號開頭的變數是洞（hole），代表還沒完成的值。
> 我們可以用 Idris 檢查這些洞是屬於什麼型態，它也會告訴我們目前環境中既有的值各別是什麼型態，提供參考。

### 定義函式的型態

第一步就是先定義 `shrink` 函式的型態。
在這種能夠表達依值型態的強大型態系統中，挑選正確適合的型態是非常重要的步驟。
因為型態本身包含足夠多的資訊，當我們定義好型態之後，我們甚至可以配合程式的型態推論來輔助編寫剩下的內容。
我們會在更之後的步驟中感受到這一點。

1. 既然要刪掉某個元素，傳入的第一個參數必須是一個長度非零的列表
- 所以必須有型態 `Vect (S n) a`
- 參數的模式確定只會是 `y :: ys`
2. 第二個參數代表命題「某個元素 `x` 在列表 `xs`」的證明
- 所以有型態 `Elem x xs`
- 這裡的 `xs` 依賴於第一個參數的值，所以在型態 `Vect (S n) a` 前面特別將值標註出來，並取同樣的名稱 `xs`
3. 最後回傳的將是第一個參數刪掉一個元素後的列表
- 所以會有型態 `Vect n a`
- 長度減一而從 `S n` 變為 `n`
- 其他元素的型態不變，依然屬於型態 `a`

綜合以上的要求，我們於是就定義出了 `shrink` 函式的型態：

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (y :: ys) p0 = ?result

### 分析參數

接著我們開始定義函式內容。
先針對參數 `p0`，它屬於 `Elem x xs`，也就是說 `p0` 是「元素 `x` 在列表 `xs` 裡」的「證明」。
由於型態 `Elem x xs` 的定義分成兩類，所以我們用模式比對來分情況處理：
- 參數值 `p0` 是 `Here`
- 表示元素 `x` 在列表 `xs`（也就是 `y :: ys`）的第一項
- 就代表參數中的 `y` 就是 `x`
- 既然要刪除的東西在第一項，回傳值直接就是剩下的 `ys` 了
- 參數值 `p0` 是 `There p`
- 表示元素 `x` 在列表 `xs`（也就是 `y :: ys`）的後面
- 就代表元素 `x` 在列表 `ys` 裡面
- 根據 `There` 的定義，`p` 是屬於型態 `Elem x ys`
- 正是「元素 `x` 在列表 `ys` 裡」的「證明」

於是我們有了下面的程式碼：

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys) Here      = ys
shrink (y :: ys) (There p) = ?result

下一步我們為第三行未解決的情況進一步分析 `ys`。
因為 `y :: ys`（也就是 `xs`）屬於型態 `Vect (S n) a`，所以根據 `(::)` 的定義，`ys` 就會屬於 `Vect n a` 型態。
這裡代表長度的 `n` 並沒有額外限制，表示 `ys` 有可能是空列表 `[]`，也可能不是。
所以對於 `ys`，我們也用模式比對來分情況處理：
- `ys` 是 `[]`
- `ys` 有模式 `z :: zs`
- 因為 `z :: zs` 不是空列表，我們可以用遞迴的方式呼叫 `shrink`
- 保留第一個項 `y`，並接上從 `z :: zs` 去掉元素 `x` 後的結果
- `shrink` 函式要用到「元素 `x` 在列表 `z :: zs` 裡」的「證明」`p`

於是程式碼變成了這個樣子：

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys)      Here      = ys
shrink (y :: [])      (There p) = ?result
shrink (y :: z :: zs) (There p) = y :: shrink (z :: zs) p

### 用 `Void` 處理不可能的模式

最後我們剩下了第 3 行那個不可能的狀況：我們有一個「證明」`p` 說要移除的元素 `x` 在空列表 `[]` 裡面。
這時我們可以檢查，`p` 的型態的確因為參數的型態而被確定為沒有值的 `Elem x []`。
我們或許可以不寫第 3 行，但這會讓這個函式變成部分函式，那我們只能依靠信心與勇氣確定程式不會撞到這個未實現的結果而壞掉。

不過，現在我們有 `Void`，我們的型態系統有能力知道 `p` 其實是個不會存在的值。
並且我們有【爆炸原理】，就如同在邏輯中用它解決矛盾的分支狀況，我們也能用 `absurd` 造出任何想要的東西，包括移除元素後的列表！
「我知之濠上也！」

shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a
shrink (x :: ys)      Here      = ys
shrink (y :: [])      (There p) = absurd p
shrink (y :: z :: zs) (There p) = y :: shrink (z :: zs) p