是的，你基本上是对的。
子类型是两种类型之间的关系。它本身并没有说明这种关系实际上如何应用于表达式的类型。
包含通常意味着存在允许将子类型隐式应用于其类型的表达式的类型规则。有些语言具有子类型但没有包含规则，并且必须使用特殊类型注释（例如 OCaml）显式调用它。
子类型化是否是“强制的”也有一定的独立性。强制子类型会更改其所应用的值。例如，在语言中Int <: Float，子类型可能是强制的，因为整数和浮点数是不同的域。对象上典型的 OO 风格子类型通常是非强制的。然而，这是一个有点模糊的概念，因为它通常取决于语义模型的选择，并且不一定会产生可观察到的差异（除非语言允许使用向下转换来反转子类型）。在实践中，它更多地指的是实现技术而不是语义。