#type-theory #subtyping
#теория типов #подтипирование
Вопрос:
В чем разница между подтипом и подчинением? Подчинение означает неявное принуждение?
Ответ №1:
Да, вы в основном правы.
Подтипирование — это отношение между двумя типами. Само по себе это не говорит о том, как это отношение на самом деле применяется к типизации выражений.
Подчинение обычно означает наличие правила типизации для выражений, которое позволяет применять подтипы к их типам неявно. Существуют языки, в которых есть подтипирование, но нет правила подчинения, и где оно должно вызываться явно со специальной аннотацией типа (например, OCaml).
Существует также несколько независимый аспект того, является ли подтипирование «принудительным». Принудительное подтипирование изменяет значение, к которому оно применяется. Например, в языке, где Int <: Float
подтипирование может быть принудительным, потому что целые числа и значения с плавающей точкой — это разные домены. Типичное подтипирование объектов в стиле OO обычно не является принудительным. Однако это несколько расплывчатое понятие, поскольку оно часто зависит от выбора семантической модели и не обязательно может иметь заметное значение (если только язык не позволяет отменить подтипирование с понижением). На практике это относится скорее к методам реализации, чем к семантике.