I don't know what the procedure means (I've seen this a few times but not sure where it came from... links appreciated) - takes in a procedure that takes itself as a parameter?  The lambda probably behaves differently pending on the parameter - doesn't this fall under dependent type?  I will pass on more counter examples as I know I can't type them all and hence want a good type system :) I assume you are trying to say that you can't type everything under the sun that you can evaluate, correct?  Is this a limitation of a type system, or an inherent limitation in type theory?  Thanks, yc <div>On 6/11/07, Prabhakar Ragde <<a href="mailto:plragde@uwaterloo.ca">plragde@uwaterloo.ca</a>> wrote:<blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;"> YC wrote: > add1 is int -> int > (lambda (x) x) is any -> any > I don't understand enough about call/cc so I won't attempt  ;) Okay, so try to type (lambda (x) (x x)) from Eli Barzilay's .signature. --PR _________________________________________________   For list-related administrative tasks:   <a href="http://list.cs.brown.edu/mailman/listinfo/plt-scheme">http://list.cs.brown.edu/mailman/listinfo/plt-scheme</a> </blockquote></div>