topics/_week5_system_F.mdwn

   1 # System F and recursive types
   2
   3 In the simply-typed lambda calculus, we write types like <code>&sigma;
   4 -> &tau;</code>.  This looks like logical implication.  We'll take
   5 that resemblance seriously when we discuss the Curry-Howard
   6 correspondence.  In the meantime, note that types respect modus
   7 ponens:
   8
   9 <pre>
  10 Expression    Type     Implication
  11 ----------------------------------
  12 fn            &alpha; -> &beta;   &alpha; &sup; &beta;
  13 arg           &alpha;             &alpha;
  14 ------        ------              --------
  15 fn arg        &beta;              &beta;
  16 </pre>
  17
  18 The implication in the right-hand column is modus ponens, of course.
  19
  20 System F is usually attributed to Girard, but was independently
  21 proposed around the same time by Reynolds.  It enhances the
  22 simply-typed lambda calculus with quantification over types.  In
  23 System F, you can say things like
  24
  25 <code>&Lambda; &alpha; (\x.x):(&alpha; -> &alpha;)</code>
  26
  27 This says that the identity function maps arguments of type &alpha; to
  28 results of type &alpha;, for any choice of &alpha;.  So the &Lambda; is
  29 a universal quantifier over types.
  30