title: How to systematically compute the number of inhabitants of a given type?
body: <p>How to systematically compute the number of inhabitants of a given type in System F?</p>
  
  <p>Assuming the following restrictions:</p>
  
  <ul>
  <li>All inhabitants terminate, i.e. no bottom.</li>
  <li>All inhabitants lack side-effects.</li>
  </ul>
  
  <p>For example (using Haskell syntax):</p>
  
  <ul>
  <li><code>Bool</code> has two inhabitants.</li>
  <li><code>(Bool, Bool)</code> has four inhabitants.</li>
  <li><code>Bool -&gt; (Bool, Bool)</code> has sixteen inhabitants.</li>
  <li><code>forall a. a -&gt; a</code> has one inhabitant.</li>
  <li><code>forall a. (a, a) -&gt; (a, a)</code> has four inhabitants.</li>
  <li><code>forall a b. a -&gt; b -&gt; a</code> has one inhabitant.</li>
  <li><code>forall a. a</code> has zero inhabitants.</li>
  </ul>
  
  <p>Implementing an algorithm for the first three is trivial, but I can't figure out how to do it for the other ones.</p>