I'm trying to grook Haskell singletons.
In the paper Dependently Typed Programming with Singletons and in his blog post singletons v0.9 Released! Richard Eisenberg defines the data type Nat which defines natural numbers with the peano axioms:
data Nat = Zero | Succ Nat
By using the language extension DataKinds this data type is promoted to the type level. The data constuctors Zero and Succ are promoted to the type constructors 'Zero and 'Succ. With this we get for every Natural number a single and unique corresponding type on the type level. Eg for 3 we get 'Succ ( 'Succ ( 'Succ 'Zero)). So we have now Natural numbers as types.
He then defines on the value level the function plus and on the type level the type family Plus to have the addition operation available. With the promote function/quasiqoter of the singletons library we can automatically create the Plus type family from the plus function. So we can avoid writing the type family ourselfs.
So far so good!
With GADT syntax he also defines a data type SNat:
data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)
Basically he only wraps the Nat type into a SNat constructor. Why is this necessary? What do we gain? Are the data types Nat and SNat not isomorphic? Why is SNat a singleton, and why is Nat not a singleton? In both cases every type is inhabited by one single value, the corresponding natural number.