В чем разница между подтипом и подчинением?

#type-theory #subtyping

#теория типов #подтипирование

Вопрос:

В чем разница между подтипом и подчинением? Подчинение означает неявное принуждение?

Ответ №1:

Да, вы в основном правы.

Подтипирование — это отношение между двумя типами. Само по себе это не говорит о том, как это отношение на самом деле применяется к типизации выражений.

Подчинение обычно означает наличие правила типизации для выражений, которое позволяет применять подтипы к их типам неявно. Существуют языки, в которых есть подтипирование, но нет правила подчинения, и где оно должно вызываться явно со специальной аннотацией типа (например, OCaml).

Существует также несколько независимый аспект того, является ли подтипирование «принудительным». Принудительное подтипирование изменяет значение, к которому оно применяется. Например, в языке, где Int <: Float подтипирование может быть принудительным, потому что целые числа и значения с плавающей точкой — это разные домены. Типичное подтипирование объектов в стиле OO обычно не является принудительным. Однако это несколько расплывчатое понятие, поскольку оно часто зависит от выбора семантической модели и не обязательно может иметь заметное значение (если только язык не позволяет отменить подтипирование с понижением). На практике это относится скорее к методам реализации, чем к семантике.