Why are these two tuples in idris equal?

6
votes

I am reading Type driven development with Idris, and one of the exercises asks the reader to define a type TupleVect, such that a vector can be represented as:

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

I solved it by defining the following type:

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

The following test typechecks:

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

My question is, why is (1,2,3,4,()) == (1,(2,(3,(4,()))))? I would have thought that the right hand side is a 2-tuple, consisting of an Int and another tuple.

1
idris
could it be because (x,y,z) is syntactic sugar for (x,(y,z))? – marcosh

1 Answers

7
votes

Checking the documentation at http://docs.idris-lang.org/en/latest/tutorial/typesfuns.html#tuples, you can see that tuples are represented as nested pairs.

Hence (x, y, z) == (x, (y, z)) for every x, y, z