title: What's the absurd function in Data.Void useful for?
body: <p>The <a href="http://hackage.haskell.org/packages/archive/void/0.5.10/doc/html/Data-Void.html#v:absurd"><code>absurd</code></a> function in <code>Data.Void</code> has the following signature, where <code>Void</code> is the logically uninhabited type exported by that package:</p>
  
  <pre><code>-- | Since 'Void' values logically don't exist, this witnesses the logical
  -- reasoning tool of \"ex falso quodlibet\".
  absurd :: Void -&gt; a
  </code></pre>
  
  <p>I do know enough logic to get the documentation's remark that this corresponds, by the propositions-as-types correspondence, to the valid formula <code>⊥ → a</code>.</p>
  
  <p>What I'm puzzled and curious about is: in what sort of practical programming problems is this function useful?  I'm thinking that perhaps it's useful in some cases as a type-safe way of exhaustively handling "can't happen" cases, but I don't know enough about practical uses of Curry-Howard to tell whether that idea is on the right track at all.</p>
  
  <p>EDIT: Examples preferably in Haskell, but if anybody wants to use a dependently typed language I'm not going to complain...</p>