How does TypeId work in the AM?

[digama0]

The interesting questions that TypeId presents are:

• When are two types "definitely the same" for TypeId purposes? This should correspond roughly to equality of mangled type names, and involves erasure of lifetimes and some kind of valtree thing for constants.
• How do we square this with the fact that TypeId is manifestly, observably finite? This is of course the underlying theoretical issue behind Collisions in type_id rust#10389 . I assume we want the spec to say that rustc is not conforming here, since otherwise proving the soundness of the type system goes out the window since it's demonstrably false, but we also don't want the spec to be literally unimplementable so we have to be careful.

[scottmcm]

• How do we square this with the fact that TypeId is manifestly, observably finite?

I don't know that this is really a problem any more than there being a macro recursion limit or string literal length limit or the machine being only able to address finite memory. The layout of TypeId isn't specified, so it can be assumed to always be big enough to represent every type in the program. And if you're dynamically loading types, well, it's no worse than dynamically loading functions, where you'll also run out of space at some point.

[digama0]

I think that makes sense, the compiler is always allowed to fail "spuriously" at either compile time or run time due to encroaching resource limits. The problem in current rustc is that it makes no attempt to detect or do something to avoid the error case, but it is conceivable that a different, more naive implementation (for example, implementing TypeId as &'static str pointing to the mangled name) could work (although I think name mangling also has hash collision issues in crate names), so perhaps it wouldn't be such a big deal to specify essentially that as the "official" AM implementation and treat anything else as an optimization which should be observably equivalent.

I think the reason that the TypeId issue has been so hard to solve is that it structurally requires a kind of coherence under adding more crates later that makes the obvious algorithm "just sequentially number everything, there are only finitely many types anyway" not implementable. I'm not entirely sure whether the AM version of the problem faces similar issues: you can use nondeterminism to say "pick a magically good choice early to avoid conflicts later", which means you can make use of the whole space of IDs and then fail if there are still too many types, but I think it's not a good look if the AM gets too divorced from reality, since it's still supposed to vaguely resemble a computer and implementation plan.

[digama0]

Thinking about it some more, I think I see how to make the forward coherence issue concrete, even in the AM version: A rust crate, compiled to a rlib, may not be compatible with other crates that are separately compiled even in situations where they "should" be compatible (i.e. the types are distinct, they have the same view of common dependencies, etc.). We can only claim that there exists a choice of nondeterminism for the two compilations resulting in compatible crates; but there isn't any computable method for choosing the TypeIds in one crate such that it will agree with the choices for TypeIds in the other crate without any communication between them and such that different types don't overlap. (However we could cause a spurious failure in this case, which I guess is a link time error here, since this situation is at least detectable.)

[Diggsey]

@digama0 I think it depends on the implementation. For example, an implementation based on pointers to static memory (where the linker deduplicates that static memory to create a unique TypeId) is effectively a communication channel between otherwise unrelated crates.