type-theory - 子类型和包含有什么区别？

Question

子类型和包含有什么区别？包容是否意味着隐性强制？

Answer 1

是的，你基本上是对的。

子类型是两种类型的关系。它本身并没有说明这种关系如何实际应用于表达式的类型。

包含通常意味着表达式的类型规则的存在，该规则允许将子类型隐式应用于其类型。有些语言有子类型但没有包含规则，并且必须使用特殊类型注释（例如，OCaml）显式调用它。

子类型化是否是“强制的”也有一些独立的方面。强制子类型改变了它所应用的值。例如，在 Int < Float 的语言中，子类型化可能是强制的，因为 int 和 float 是不同的域。对象上典型的 OO 风格子类型化通常是非强制的。然而，这是一个有点模糊的概念，因为它通常取决于语义模型的选择，并且不一定会产生可观察到的差异（除非一种语言允许使用向下转换来反向细分）。在实践中，它指的是实现技术而不是语义。