What is “completeness of subtyping”

[nomeata]

The spec currently says

Completeness: Subtyping covers all cases of successful deserialisation.

and I wonder what that precisely means, and if we really want it.

(Previous discussion at #128 (comment) )

[nomeata]

The wording above suggests

(∀ v. v :? T ~> _ ⇒ v :? T' ~> _) ⇒ T <: T'

But that does not hold as stated, for two reasons:

• Any empty type would need to be a subtype of any type, e.g. opt empty <: null, or Empty <: t where type Empty = rec { Empty } or vec Empty <: vec t
• Decoding of references (functions, sevices) doesn't actually fail eagerly, but causes subsequent uses of such a reference to fail.

One attempt might be “Subtyping is the largest relation that is transitive and sound (in the sense of the IDL-Soundness document)”. This is quite declarative and realtively elegant, I think, and I believe it implies the local soundess of deserialization.

It still requires Empty <: t, but it seems all “natural” definitions will lead to that. If we want to rule out that then maybe we have to do say something handwavy like “, … with exceptions for types that contain empty types”.

Maybe allowing Empty <: t and variant {} <: t isn’t actually so bad?