[btilly]

It is impossible. Dynamically typed programs are able to look at the name of the type, write arbitrary Turing complete code reasoning about it, and then do whatever they want with it.

For example a unit test framework might walk your class hierarchy, identify all classes whose name matches a particular pattern, and then start doing stuff with that.

Of course there is always a way to accomplish the same thing without abusing the type system. But as soon as you do so, it is a different program.

[lmm]

Many type systems allow encoding arbitrary Turing complete code, so that doesn't necessarily imply typing those programs correctly is impossible.

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