title: Algebraically interpreting polymorphism
body: <p>So I understand the basic algebraic interpretation of types:</p>
  
  <pre><code>Either a b ~ a + b
  (a, b) ~ a * b
  a -&gt; b ~ b^a
  ()   ~ 1
  Void ~ 0 -- from Data.Void
  </code></pre>
  
  <p>... and that these relations are true for concrete types, like <code>Bool</code>, as opposed to polymorphic types like <code>a</code>.  I also know how to translate type signatures with polymorphic types into their concrete type representations by just translating the Church encoding according to the following isomorphism:</p>
  
  <pre><code>(forall r . (a -&gt; r) -&gt; r) ~ a
  </code></pre>
  
  <p>So if I have:</p>
  
  <pre><code>id :: forall a . a -&gt; a
  </code></pre>
  
  <p>I know that it does not mean <code>id ~ a^a</code>, but it actually means:</p>
  
  <pre><code>id :: forall a . (() -&gt; a) -&gt; a
  id ~ ()
     ~ 1
  </code></pre>
  
  <p>Similarly:</p>
  
  <pre><code>pair :: forall r . (a -&gt; b -&gt; r) -&gt; r
  pair ~ ((a, b) -&gt; r) - &gt; r
       ~ (a, b)
       ~ a * b
  </code></pre>
  
  <p>Which brings me to my question.  What is the "algebraic" interpretation of this rule:</p>
  
  <pre><code>(forall r . (a -&gt; r) -&gt; r) ~ a
  </code></pre>
  
  <p>For every concrete type isomorphism I can point to an equivalent algebraic rule, such as:</p>
  
  <pre><code>(a, (b, c)) ~ ((a, b), c)
  a * (b * c) = (a * b) * c
  
  a -&gt; (b -&gt; c) ~ (a, b) -&gt; c
  (c^b)^a = c^(b * a)
  </code></pre>
  
  <p>But I don't understand the algebraic equality that is analogous to:</p>
  
  <pre><code>(forall r . (a -&gt; r) -&gt; r) ~ a
  </code></pre>