[lmm]

> That is not what btilly means. You are talking about using a type system to write an arbitrary program. btilly is talking about using an arbitrary program to specify the typing rules for a set of values. His assertion is correct: if you can use an arbitrary program to determine what the types are in your program, then figuring out the types of your program is undecidable.

Right, but my point is that it's not necessarily impossible to just express the program that figures out the type in the type system.

[scott_s]

I'm not quite sure what you mean. Being able to "express the program" (which I take to mean a human writes the program) is independent of being able to statically verify what it does.