title: Encoding "Less Than" with Haskell
body: <p>am hoping some Haskell experts can help clarify something.</p>
  
  <p>Is it possible to define <code>Nat</code> in the usual way (via @dorchard <a href="https://stackoverflow.com/questions/16017294/singleton-types-in-haskell">Singleton types in Haskell</a>)</p>
  
  <pre><code>data S n = Succ n 
  data Z   = Zero
  
  class Nat n 
  instance Nat Z
  instance Nat n =&gt; Nat (S n)
  </code></pre>
  
  <p>(or some variant thereof) and then define a <code>LessThan</code> relation 
  such that forall <code>n</code> and <code>m</code></p>
  
  <pre><code>LessThan Z (S Z)
  LessThan n m =&gt; LessThan n     (S m)
  LessThan n m =&gt; LessThan (S n) (S m)
  </code></pre>
  
  <p>and then write a function with a type like:</p>
  
  <pre><code>foo :: exists n. (LessThan n m) =&gt; Nat m -&gt; Nat n
  foo (S n) = n
  foo Z     = foo Z
  </code></pre>
  
  <p>I explicitly want to use the "LessThan" in the output type for <code>foo</code>,
  I realize that one could certainly write something like </p>
  
  <pre><code>foo :: Nat (S n) -&gt; Nat n
  </code></pre>
  
  <p>but thats not what I'm after.</p>
  
  <p>Thanks!</p>
  
  <p>Ranjit.</p>