Как думать о полиморфизме с подтипами

Принцип замещения Лисков гласит:

Инварианты супертипа должны сохраняться в подтипе.

Меня особенно интересует пересечение этого принципа и полиморфизма. В частности, полиморфизм подтипов, хотя на самом деле это похоже на параметрический полиморфизм и классы типов Haskell.

Итак, я знаю, что функции являются подтипами, когда их аргументы контравариантны, а типы возвращаемых значений ковариантны. Мы можем предположить, что методы — это просто функции с неявным аргументом «я». Однако это, по-видимому, означает, что если подкласс переопределяет метод родителя, он больше не является подтипом, поскольку один из его методов больше не является подтипом.

Например. Возьмите следующий псевдокод:

class Parent:
    count : int
    increment : Parent -> ()
    {
        count += 1
    }

class Child inherits Parent:
    increment : Child -> ()
    {
        count += 2
    }

Итак, возвращаясь к LSP: можем ли мы сказать, что свойство Parent.increment() должно сохраняться для Child.increment(), даже если эти два не подчиняются строгому отношению подтипа?

В более общем плане мой вопрос таков: как правила подтипирования взаимодействуют с более конкретными аргументами полиморфных функций и как правильно думать об этих двух концепциях вместе?


person Sam Pattuzzi    schedule 25.07.2014    source источник


Ответы (2)


Цитата из статьи Википедии о принципе замещения Лисков

Более формально, принцип подстановки Лискова (LSP) — это частное определение отношения подтипа, называемое (strong) поведенческим подтипом [...]

Поведенческий подтип — это более сильное понятие, чем типичное подтипирование функций, определенных в теории типов, которое опирается только на контравариантность типов аргументов и ковариантность возвращаемого типа. Поведенческие подтипы в общем случае тривиально неразрешимы [...]

Существует ряд поведенческих условий, которым должен соответствовать подтип:

  • Предусловия не могут быть усилены в подтипе.
  • Постусловия не могут быть ослаблены в подтипе.
  • Инварианты супертипа должны быть сохранены в подтипе.

Таким образом, LSP является более сильным определением подтипов, которое опирается на функции, выходящие за рамки теории типов.

В вашем примере это повышается и падает на ваш инвариант.

calling increment will increase count by **exactly 1**

Очевидно, что Child не может быть выражен через Parent, так как инвариант нарушен. Это не может быть выведено только из синтаксиса.

LSP должен привести вас к раздельному определению родительского и дочернего элементов, поскольку они оба наследуются от Incrementable, который имеет более слабое пост-условие.

person Community    schedule 25.07.2014
comment
Мой вопрос больше о семантике аргумента. LSP утверждает, что инвариант верен для подтипа тогда и только тогда, когда он верен для супертипа. Отношение подтипа утверждает, что для функций a -> b <: c -> d тогда и только тогда, когда c <: a и b <: d. Согласно этому определению подтипа, Child.increment() не является подтипом Parent.increment(). Поэтому, почему следует применять LSP? - person Sam Pattuzzi; 25.07.2014
comment
Правильный способ мышления состоит в том, что LSP является ориентиром для тех случаев, когда полиморфизм имеет смысл, а НЕ как его логическое/математическое свойство. Полиморфизм дает вам машину. LSP говорит, что вы должны ездить только по дорогам. Ты говоришь: «Эй, смотри, я еду по тротуару». ЛСП сломался. Это? - person Sirotnikov; 26.07.2014
comment
Насколько я понял, Лисков сама дала этому принципу очень теоретическое и математическое обоснование. По этому поводу написано множество статей. Итак, на этом основании я не согласен с вашим предположением, что LSP — это всего лишь рекомендация. - person Sam Pattuzzi; 29.07.2014
comment
Что ж, честно говоря, ваш вопрос сформулирован таким образом, что его легко интерпретировать как философский вопрос, а не как жесткий теоретический вопрос. Но, возможно, это моя предвзятость. Прошло много времени с тех пор, как я брал уроки теории типов, но я никогда не помню, чтобы теория была «правильной». В любом случае на ваш теоретический вопрос дан ответ в принципе замещения Лисков: я отредактирую свой ответ. - person Sirotnikov; 30.07.2014
comment
Спасибо. Из моего вопроса было не совсем понятно. Я думаю, что этот ответ очень хорош. Один момент для уточнения: тип, на который ссылается ссылка, относится к типу класса, а не к методу класса. Например: increment will increase count не имеет смысла как свойство метода, потому что возникает вопрос, что такое count? Следствием этого является то, что: Child.increment : Parent -> (), а не Child.increment : Child -> (). На самом деле это один метод, который ведет себя по-разному для разных типов (логически говоря). - person Sam Pattuzzi; 30.07.2014
comment
Честно говоря, я привык к менее формальному обсуждению этих вопросов, так что извините меня, если я не понял, что вы имеете в виду. Я смотрю на increment will increase count не обязательно как на свойство метода, а как на инвариант класса. Таким образом, он должен полагаться на внутреннее знание класса, поскольку мы никогда не определяем никаких внешних результатов для int count. getCount() метода нет. С философской точки зрения, если внутреннее состояние Parent (т.е. int count) никогда не влияет на внешний мир - что-то на самом деле сломано? - person Sirotnikov; 31.07.2014
comment
Здесь не нарушен ни один инвариант. Только (возможное) постусловие. - person Elazar; 31.07.2014

Термин «подтипирование» технически является синтаксическим вопросом. Таким образом, синтаксически Child <: Parent.

Принцип Лисков касается поведенческих подтипов, как отмечено в Википедии. Это требует синтаксического подтипа, но это также зависит от вашего определения инварианта класса и условий до/после. Поскольку вы ничего не определили, говорить о нарушениях бессмысленно.

Если вы определяете постусловие increment как new count = old count + 1, имеет место нарушение.

Если вы определите постусловие increment как new count > old count, его не будет.

В общем, определение постусловия как «точно постусловия родителя» делает полиморфизм включения невозможным по определению. Там, где полиморфизм имеет смысл, следует смягчить определение постусловия.

Обратите внимание, что инвариант класса касается возможных значений — моментального снимка объекта — и, поскольку вы можете определить increment ребенка в терминах increment родителя, он не может нарушить какой-либо инвариант.

person Elazar    schedule 31.07.2014