[PL-sem-jr] Followup on today's talk

[Felix S. Klock II]

All-

Just some notes in response to some of the issues that we talked about
today.

1. I'm am confident that in lambda_mu, the statement M : sigma_0 is
   derivable with an empty basis for any closed M 
   (where approx is the curly-equals that I was using
      and sigma_0 is chosen such that 
		     sigma_0 approx sigma_0 -> sigma_0
    ).
   Such a sigma_0 : (mu alpha . (alpha -> alpha))

   Just remember the key lambda-mu rule:

        Gamma |- M : sigma       sigma approx tau
   -----------------------------------------------
                  Gamma |- M : tau



   * Here is a sample derivation for \x . x x

   x : sigma_0 |- x : sigma_0 -> sigma_0
   x : sigma_0 |- x x : sigma_0
   |- \x . x x : sigma_0 -> sigma_0
   |- \x . x x : sigma_0



   * Here is a sample derivation for \x . x

   x : sigma_0 |- x : sigma_0
   |- \x . x : sigma_0 -> sigma_0
   |- \x . x : sigma_0

   And so on.

2. I still do not believe that this means that you can show that 
	     sigma_0 approx tau for all tau

   In particular, mu alpha . alpha -> gamma does not yield the same
   tree as        mu alpha . alpha -> alpha

   A funny thing about lambda-mu and lambda-cap (intersection types)
   is just because you can infer that some type sigma exists and is
   ascribable to a term (e.g. sigma_0) doesn't mean that sigma is a
   variant of the type tau that you INTENDED to infer; I think this is
   the sort of useful property that having principal types buys you.

3. I am aware that my attempt to explain why you can't stuff type
   schemes into lambda parameters (but you *CAN* stuff them as
   let-bindings in Hindley-Milner) was not very clear.

   My only excuse on this front is that this is a hard thing to show.
   Even Barendregt didn't have a proof available of whether the type
   inference was undecidable for Lambda-2 at the time that he wrote
   this chapter of the handbook; only the result that the problem of
   type inference is reducible to the problem of type checking, whose
   decidability was also unknown at the time.  (Barendregt explicitly
   quotes Robin Milner in calling them both "embarressing open
   problems")

   For the actual undecidability result, you need to see Joe Wells
	    http://www.cee.hw.ac.uk/~jbw/papers/
   "Typability and type checking in the second-order lambda -calculus
    are equivalent and undecidable."

   Note that Wells' proof is really really hard to get through.  To
   me, that implies that it is thus really really hard to explain why
   putting type schemes into the lambda terms is problematic.  (At
   least for the pure Curry style.  As some have discussed, it seems
   reasonable to work out a variant in the Church style where explicit
   polymorphism is allowed while inferred types are forced to be
   monomorphic.  Several languages have been implemented that employ
   such an approach in one way or another).

   I wrote a newsgroup posting last year for HoPL summarizing what I
   managed to get out of the Wells' paper.  If you are interested in
   seeing that, drop me a line, and I will forward that posting out of
   my sent-messages folder.

4. I have a copy of Barendregt's chapter at:
   /proj/will/pnkfelix/Papers/barendregt92lambda.ps.gz

   Its also available online at:
   http://citeseer.ist.psu.edu/barendregt92lambda.html

-Felix