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

以下测试类型检查:

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