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