[scott_s]

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.

Again, this is different from using a type system to write an arbitrary program. But, it is true that type systems which allow you to write arbitrary programs are undecidable. Because it's possible that such programs written in the type system cannot finish, then they cannot be well-typed. Most programs will be okay, and can be verified to be well-typed, but there still exist some that cannot be.

[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.