为什么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