title: Intuition behind encoding double negation with bottom type Nothing
body: <p>Shapeless encodes <a href="https://github.com/milessabin/shapeless/blob/85fb65f49352f7e80392b5aa8a749444e0532ce8/core/src/main/scala/shapeless/package.scala#L30" rel="nofollow noreferrer">double negation</a> like so</p>
  
  <pre><code>type ¬[T] = T =&gt; Nothing
  type ¬¬[T] = ¬[¬[T]]
  </code></pre>
  
  <p>that is</p>
  
  <pre><code>(T =&gt; Nothing) =&gt; Nothing
  </code></pre>
  
  <p>Miles <a href="https://milessabin.com/blog/2011/06/09/scala-union-types-curry-howard/" rel="nofollow noreferrer">explains</a> </p>
  
  <blockquote>
    <p>...the bottom type (Scala’s <code>Nothing</code> type) maps to logical falsehood... negation of a type <code>A</code> (I’ll write it as <code>¬[A]</code>) to have as it's values everything which isn’t an instance of <code>A</code></p>
  </blockquote>
  
  <p><code>Nothing</code> is also used to represent <a href="https://stackoverflow.com/a/35850650/5205022">non-termination</a>, that is, computation that cannot produce a value</p>
  
  <pre><code>def f[T](x: T): Nothing = f(x)
  </code></pre>
  
  <p>Applying this interpretation to <code>(T =&gt; Nothing) =&gt; Nothing</code>, it seems to mean:</p>
  
  <pre><code>(          T                   =&gt;                Nothing           )    =&gt;          Nothing 
  Assuming a value of type T,   then   the program does not terminate,   hence  it never produces a value.
  </code></pre>
  
  <p>Is this intuition correct? Are concepts of falsehood and non-termination equivalent? If so, why having a program that does not produce a value, which does not produce a value, means we have a value of T?</p>