xoltar (3) [Avatar] Offline
Hi Edwin,

First, this is great, thanks so much for writing it.

On page 183 in version 9, we define SchemaType, and in particular this clause:

SchemaType (x .+. y) = (SchemaType x, SchemaType y)

Because of this, I was surprised to find out that Idris collapses nested tuples, both at type and value level. E.g:

??> (1, (2,3))
(1, 2, 3) : (Integer, Integer, Integer)

As opposed to most languages, here's Haskell for instance:

Prelude> (1, (2,3))

It might be worth a sentence or two to note the difference and possibly explain why Idris does it this way.


Edwin Brady (66) [Avatar] Offline
This is explained in Chapter 2, although a note here referring back with a reminder is probably useful too.
Allan J Cooper (4) [Avatar] Offline
I found the SIDEBAR note in chapter 2 confusing as well, if the language DEFINES (a, b, c) as (a, (b, c)) that should be noted because most people would assume that those are equivalent but not "the same".