title: Is it possible to type `min` in a normalizing theory such as System-F or the Calculus of Constructions?
body: <p>This <code>min</code> definition below works on two church numbers and returns the least big. Each number becomes a continuation that sends its pred to the other, zig and zag, until zero is reached. Moreover, one of the numbers appends f to the result each time it is called, so, in the end, you'll have <code>(\ f x -&gt; f (... (f (f x)) ...))</code> where the number of 'f's on the right is the number of times the first continuation was called.</p>
  
  <pre><code>min a b f x = (a_continuator b_continuator)
      a_continuator = (a (\ pred cont -&gt; (cont pred)) (\ cont -&gt; x))
      b_continuator = (b (\ pred cont -&gt; (f (cont pred))) (\ cont -&gt; x))
  </code></pre>
  
  <p>It seems like <code>min</code> can't be typed on System-F. For example, in order to run it on GHC, I had to use <code>unsafeCoerce</code> twice:</p>
  
  <pre><code>import Unsafe.Coerce
  
  (#)   = unsafeCoerce
  min'  = (\ a b f x -&gt; (a (\ p c -&gt; (c # p)) (\ c -&gt; x) (b (\ p c -&gt; (f (c # p))) (\ c -&gt; x))))
  toInt = (\ n -&gt; (n (+ 1) 0))
  main  = print (toInt (min'
      (\ f x -&gt; (f (f (f (f (f x))))))               -- 5
      (\ f x -&gt; (f (f (f (f (f (f (f (f x))))))))))  -- 8
      :: Int)
  </code></pre>
  
  <p>Is it possible to type <code>min</code> on System-F (or the Calculus of Constructions)?</p>