爲什麼idris中的這兩個元組相等？

Question

我讀Type driven development with Idris，和的一個練習要求讀者限定，使得隨着一個矢量可以表示一個類型TupleVect，：

TupleVect 2 ty = (ty, (ty,())) 

我解決它通過定義以下類型：

TupleVect : Nat -> Type -> Type 
TupleVect Z ty =() 
TupleVect (S k) ty = (ty, TupleVect k ty) 

以下測試typechecks：

test : TupleVect 4 Nat 
test = (1,2,3,4,()) 

我的問題是，爲什麼(1,2,3,4,()) == (1,(2,(3,(4,()))))？我會認爲右側是一個2元組，由Int和另一個元組組成。

Answer 1

檢查文檔http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples，可以看到元組表示爲嵌套對。

因此(x, y, z) == (x, (y, z))每x，y，z