Вопрос о LSP (принцип подстановки Лискова) и подтипах

Question

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?

Answer 1

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)) - это реализация, поэтому у нас остаются менее семантические подписи в виде интерфейсов , и классы , которые наследуют для целей реализации и реализуют интерфейсы, которые им нравятся, без возможности проверить, правильно ли они это делают.

Исследователи пытались определить формальные языки для определения типов, поэтому инструменты могут проверить, соответствует ли реализация определениям типов, но усилия настолько велики, что было бы полезно скомпилировать формальный язык в исполняемый код Это ситуация Catch-22 , которая, я думаю, никогда не будет решена.

Возвращаясь к вашему первоначальному вопросу, на языках, которые допускают то, что сегодня называется «Duck Typing», ответ неразрешим, потому что объект любого типа может быть передан любой функции, и набор будет правильным, если правильные сигнатуры реализовано и результат правильный. Позвольте мне объяснить ...

На языке, подобном Eiffel , вы можете поместить постусловие на List.append(), которое List.length() должно увеличиться после операции. Так не работают языки вроде Perl, JavaScript, Python или даже Java. Это отсутствие строгости типов допускает гораздо более сжатый код, чем более строгие определения типов.

Answer 2

Это не имеет смысла; ваше утверждение с использованием and симметрично по S и T. Но я думаю, что вы хотели сказать следующее

Если для любого предложения q, такого, что q (x) доказуемо для всех x типа T, то q (y) также доказуемо для всех y: типа S, чем мы можем считать S подтипом T.

Я бы предпочел использовать математическую логику, а не неформальный английский, но если я правильно понял определение, это поведенческий подтип , который в наши дни часто называют «типизацией утки». Это очень хороший принцип подтипирования, и он снова приводит к мысли, что в любом контексте, который ожидает значение типа T, вы можете вместо этого предоставить значение типа S, и это нормально, потому что значение типа S гарантированно удовлетворяет всем свойствам, ожидаемым контекстом.

Answer 3

Я думаю, нет, вы не можете использовать это как определение.Кроме того, если q (x) истинно для любого x из T и q (y) верно для любого y из S, это также может означать, что T является подтипом S.

Чтобы быть уверенным, что являетсяподтип которого (при условии, что вы знаете, что между ними существуют отношения наследования), вы также должны знать кое-что о том, что является более «родовым» или более «специализированным», чем другие.