[Haskell-cafe] Re: Implementing fixed-sized vectors (using datatype algebra?)

[Richard A. O'Keefe]

On 8 Feb 2008, at 8:38 am, Dan Weston wrote:

> I know that naming is arbitrary, but...
>
> Digits in types seems ugly to me. In this case, it is also  
> redundant. Everyone but FORTRAN programmers counts from 0, not 1.  
> Nat and Pos seem clear. Nat0 could even mean Nat \ {0}, the  
> opposite of what is proposed, so confusion is even increased with  
> Nat0.

For what it's worth, the Ada names for the types
     {x in Z | x >= 0}
and {x in Z | x > 0}
are "Natural" and "Positive" respectively.  Natural is useful for  
counting stuff;
Positive is useful mainly because Ada practice is to index from 1.
In Z, |N is used for natural numbers, which are defined to include 0.
In modern set theory, both the cardinal and the ordinal numbers start  
with
0, not with 1.

All things considered, I would be very upset indeed if a type called  
"Nat"
or "Natural" or something like that did not include 0.