Why Nat data type in Idris starts with 0 and not 1?

Question

Total Idris newbie question, sorry.

I've been taught in school there are natural numbers (N) and natural numbers with zero (N0).
In Idris, there is data type Nat which corresponds to N0 by definition.

What would change if there will be Nat defined as follows:

data Nat = One | S Nat
data Nat0 = Zero | Nat

I guess it's easier now, but is it mainly compiler implementation issue or formal one?

There must be cases where 0 doesn't make sense and I guess these are more complicated to define correctly now.
Or not?

Answer 1

I've seen it defined both ways, but one reason we prefer to start from zero in Idris is that it's useful for describing the size of other structures, e.g. lists or trees. Lists can have zero things in them, trees can have a height of zero, appending two zero length lists results in a zero length list.

Using your definition would be fine, just unnecessarily fiddly when using Nat to talk about properties of other structures.

In cases where zero wouldn't make sense, you could define your data type to make it impossible to have zero as an index. Here's a (contrived and untested) example where zero wouldn't make sense, trees indexed by the number of elements, with elements stored at the leaves:

data Tree : Nat -> Type -> Type where
     Leaf : ty -> Tree 1 ty
     Node : Tree n ty -> Tree m ty -> Tree (n + m) ty

Given these constructors, you'll never be able to make, say, a Tree 0 Int but you'll be able to make a Tree 1 Int or Tree 2 Int or Tree n Int for any n > 0 fine...

test1 : Tree 1 Int
test1 = Leaf 94

test2 : Tree 2 Int
test2 = Node test1 test1

test3 : Tree 3 Int
test3 = Node test1 test2

test0 : Tree 0 Int
test0 = ?no_chance