LSP говорит, что
если q(x) является доказуемым свойством объектов x типа T, то q(y) должно быть истинным для объектов y типа S, где S является подтипом T.
Я могу перефразировать это следующим образом:
q(x) истинно для любого x из T => q(y) истинно для любого y любого подтипа T
А как насчет другого утверждения?
q(x) истинно для любого x из T, а q(y) истинно для любого y из S => S является подтипом T
Имеет ли это смысл ? Можем ли мы использовать его как определение subtype ?
q(x) is true for any x of T and q(y) is true for any y of S => S is a subtype of T
Ответ Нет. Это выражение означает, что общий супертип R для S и T может быть определен, и тогда LSP (позор тому, как это имя стало общепринятым) будет выполняться для T->R и S->R.
В теории типов есть типы, которые включают семантику, и есть реализации типов, которые соблюдают семантику, возможно, путем наследования реализаций.
На практике единственный разумный способ указать семантику типа (часть q(x)) — это реализация, поэтому у нас остаются бессемантические подписи в виде интерфейсов и классы, которые наследуются в целях реализации и реализуют интерфейсы, которые им нравятся, без возможности проверить, правильно ли они это делают.
Исследователи пытались определить формальные языки для указания типов, поэтому инструменты могут проверять, соответствует ли реализация определениям типов, но усилия настолько велики, что было бы неплохо скомпилировать формальный язык в исполняемый код. . Это Уловка-22, и я думаю, что она никогда не разрешится.
Возвращаясь к исходному вопросу, в языках, допускающих то, что сегодня называется «утиным вводом», ответ неразрешим, потому что объект любого типа может быть передан любой функции, и типизация является правильной, если реализованы правильные подписи и результат правильный. Позволь мне объяснить...
В таком языке, как Eiffel, вы можете поставить постусловие на List.append(), что List.length() должно увеличиваться после операция. Так работают такие языки, как Perl, JavaScript, Python или даже Java. Это отсутствие строгости по типам позволяет писать гораздо более краткий код, чем могли бы быть более строгие определения типов.
Это не имеет смысла; ваше утверждение с использованием and симметрично в S и T. Но я думаю, вы хотели сказать следующее
Если это так, что для любого предложения q такого, что q(x) доказуемо для всех
xтипаT, то q(y) также доказуемо для всех y: типаS, то мы можем считатьSподтипомT.
Я бы предпочел использовать математическую логику, а не неформальный английский, но если я правильно понял определение, то это поведенческий подтип, который в наши дни часто называют «утиным типированием». Это очень хороший принцип создания подтипов, который снова приводит к идее, что в любом контексте, который ожидает значение типа T, вы можете вместо этого предоставить значение типа S, и это нормально, потому что значение типа S гарантированно удовлетворяет всем свойствам, которые ожидаются контекстом.
Я думаю, что нет, вы не можете использовать это как определение. Кроме того, если q(x) истинно для любого x из T и q(y) истинно для любого y из S, это может также означать, что T является подтипом S.
Чтобы быть уверенным в том, какой из них является подтипом (при условии, что вы знаете, что между ними существует отношение наследования), вы также должны знать что-то о том, что является более «общим» или более «специализированным», чем другое.
