如何理解 Agda 和 Idris 中的 Fin n 型別

1樓：

不妨從邏輯的角度來看待這個問題：

給定自然數 n，要得到 0,1,..,n 這樣的集合 Fin (suc n)，可以通過歸納定義的方式：

起始步驟：zero 是 Fin (suc n) 的成員歸納步驟：如果 m 是 Fin n 的成員，那麼 suc m 是 Fin (suc n) 的成員

也就是說，把 Fin n 的每個成員成員都加上 suc，再加上 zero，就得到了 Fin (s n)。

按照這個定義，我們可以直觀地看到 Fin n 是如何構成的：

Fin 1

zero

Fin 2

zero

suc zero

Fin 3

zero

suc zero

suc (suc zero)...

2樓：

我覺得在做型別訓練、用依賴型別的時候，使語言嚴謹化是很重要的。比如說在說「(suc (i : Fin 1)) 是乙個 Fin 3 的 element 」在我看來就很奇怪 -- 這個term 都有free variable, 怎麼會是乙個"element"?

要列舉Fin 3的就按照Fin 3定義走啊，我就不寫typing derivation了:

zero : Fin (suc 2)

suc (zero ) : Fin (suc (suc 1))

suc (suc (zero )) : Fin (suc (suc (suc 0)))

這裡我把隱式引數顯示表達了，對理解有幫助 -- 比如 zero 就肯定不屬於 Fin 3 (因為它屬於Fin 1)。

你明顯看到型別層面的和值層面的是兩個不同的構造器。

至於為什麼沒有Fin 0, 跟著定義走: Fin n 是被定義為同構於/代表 , Fin 0 就代表空集，當然不該有構造器。所以你可以看到Fin n的每個值構造器最後返回的都是 Fin (suc n), 亦即沒法inhabit Fin 0。

3樓：parker liu

Fin的定義如下：

data Fin : → Set wherezero : → Fin (suc n)suc :

(i : Fin n) → Fin (suc n)從Fin的kind來看，這個型別的kind是乙個函式，意思是給定乙個kind為N的型別，可以得到乙個kind為Set 的型別。也就是說給乙個自然數n，可以得到乙個自然數n 大小的集合，也就是Fin n是乙個自然數n 大小的集合。

zero : Fin 1

而Fin 3 則是乙個大小為3 的集合，有如下三個元素：

zeroFin 3

suc zero : Fin 3suc (suc zero) : Fin 3最特殊的是Fin 0，是乙個大小為0 的集合，其中沒有元素，所以沒有值。

所以說Fin n 可以看成是集合。以上。