LSP необходим, когда какой-то код думает, что он вызывает методы типа T, и может неосознанно вызывать методы типа S, где S extends T (то есть S наследует, наследует или является подтипом, супертип T).
Например, это происходит, когда функция с входным параметром типа T вызывается (то есть вызывается) со значением аргумента типа S. Или, когда идентификатору типа T присваивается значение типа S.
val id : T = new S() // id thinks it's a T, but is a S
LSP требует, чтобы ожидания (то есть инварианты) для методов типа T (например, Rectangle) не нарушались при вызове методов типа S (например, Square).
val rect : Rectangle = new Square(5) // thinks it's a Rectangle, but is a Square
val rect2 : Rectangle = rect.setWidth(10) // height is 10, LSP violation
Даже тип с неизменяемыми полями все еще имеет инварианты, например неизменяемые Установщики прямоугольника ожидают, что размеры будут независимо изменены, но неизменные Квадратные установщики нарушают это ожидание.
class Rectangle( val width : Int, val height : Int )
{
def setWidth( w : Int ) = new Rectangle(w, height)
def setHeight( h : Int ) = new Rectangle(width, h)
}
class Square( val side : Int ) extends Rectangle(side, side)
{
override def setWidth( s : Int ) = new Square(s)
override def setHeight( s : Int ) = new Square(s)
}
LSP требует, чтобы каждый метод подтипа S имел контравариантные входные параметры и ковариантный вывод.
Contravariant означает, что дисперсия противоречит направлению наследования, то есть тип Si каждого входного параметра каждого метода подтипа S должен быть одинаковым или супертипом типа Ti соответствующего входного параметра соответствующего метода супертипа T.
Ковариация означает, что дисперсия находится в том же направлении наследования, то есть тип So выходных данных каждого метода подтипа S, должен быть одинаковым или подтипа из тип To соответствующего выхода соответствующего метода супертипа T.
Это потому, что если вызывающий объект думает, что он имеет тип T, думает, что он вызывает метод T, он предоставляет аргумент (ы) типа Ti и назначает вывод типу To. Когда он фактически вызывает соответствующий метод S, то каждый входной аргумент Ti назначается входному параметру Si, а выход So назначается типу To. Таким образом, если бы Si не было контравариантным по отношению к W.r.t. до Ti, тогда подтип Xi - который не будет подтипом Si - может быть присвоен Ti.
Кроме того, для языков (например, Scala или Цейлон), которые имеют аннотации различий на сайте определения параметров полиморфизма типов (т. Е. Обобщения), взаимное или обратное направление аннотации дисперсии для каждого параметра типа T должно быть напротив или в том же направлении соответственно каждому входному параметру или выходу (каждого метода T), который имеет тип параметра типа.
Кроме того, для каждого входного параметра или выхода, который имеет тип функции, требуемое направление отклонения меняется на противоположное. Это правило применяется рекурсивно.
Подтип подходит для , где можно перечислить инварианты.
В настоящее время проводится много исследований о том, как моделировать инварианты, чтобы они обеспечивались компилятором.
Typestate (см. Стр. 3) объявляет и применяет инварианты состояния, ортогональные типу. Альтернативно, инварианты могут быть принудительно введены с помощью , преобразующей утверждения в типы . Например, чтобы утверждать, что файл открыт до его закрытия, File.open () может вернуть тип OpenFile, который содержит метод close (), недоступный в File. API tic-tac-toe может быть еще одним примером использования типизации для принудительного применения инвариантов во время компиляции. Система типов может даже быть полной по Тьюрингу, например Scala . Языки с независимой типизацией и доказатели теорем формализуют модели типизации высшего порядка.
Из-за необходимости семантики для абстрактного по сравнению с расширением я ожидаю, что использование типизации для модельных инвариантов, то есть унифицированная денотационная семантика высшего порядка, превосходит Typestate. «Расширение» означает неограниченную, пермутированную композицию несогласованного модульного развития. Поскольку мне кажется, что антитеза объединения и, следовательно, степени свободы, иметь две взаимозависимые модели (например, типы и Typestate) для выражения общей семантики, которые не могут быть объединены друг с другом для расширяемой композиции. , Например, Expression Problem -подобное расширение было унифицировано в областях подтипирования, перегрузки функций и параметрической типизации.
Моя теоретическая позиция заключается в том, что для знания существуют (см. Раздел «Централизация слепа и непригодна»), никогда не будет общей моделью, которая может обеспечить 100% охват все возможные инварианты на языке Тьюринга. Чтобы знания существовали, неожиданных возможностей много, то есть беспорядок и энтропия всегда должны увеличиваться. Это энтропийная сила. Чтобы доказать все возможные вычисления потенциального расширения, нужно заранее вычислить все возможные расширения.
Вот почему существует теорема Остановки, т. Е. Неразрешимо, завершается ли каждая возможная программа на языке Тьюринга. Можно доказать, что какая-то конкретная программа завершается (та, для которой все возможности были определены и вычислены). Но невозможно доказать, что все возможные расширения этой программы прекращаются, если только возможности расширения этой программы не являются полными по Тьюрингу (например, с помощью зависимой типизации). Поскольку основным требованием для полноты по Тьюрингу является неограниченная рекурсия , интуитивно понятно, как теоремы Гёделя о неполноте и парадокс Рассела применимы к расширению.
Интерпретация этих теорем включает их в обобщенное концептуальное понимание энтропийной силы:
- Теоремы Гёделя о неполноте : любая формальная теория, в которой могут быть доказаны все арифметические истины, противоречива.
- парадокс Рассела : каждое правило членства для набора, которое может содержать набор, перечисляет конкретный тип каждого члена или содержит себя. Таким образом, множества либо не могут быть расширены, либо являются неограниченной рекурсией. Например, набор всего, что не является чайником, включает в себя, включает себя, включает себя и т. Д. Таким образом, правило является непоследовательным, если оно (может содержать набор и) не перечисляет конкретные типы (т. Е. Допускает все неопределенные типы) и не допускает неограниченного расширения. Это набор наборов, которые не являются членами самих себя. Эта неспособность быть непротиворечивой и полностью перечисляемой по всем возможным расширениям является теоремой Гёделя о неполноте
- Принцип подстановки Лискова : как правило, это неразрешимая проблема, является ли какой-либо набор подмножеством другого, т.е. наследование обычно неразрешимо.
- Ссылка Линского : неразрешимо, что такое вычисление чего-либо, когда оно описывается или воспринимается, то есть восприятие (реальность) не имеет абсолютной точки отсчета.
- теорема Коуза :. Нет внешней опорной точки, таким образом, любой барьер для неограниченных возможностей внешних потерпит неудачу
- Второй закон термодинамики : вся вселенная (замкнутая система, т. Е. Все) стремится к максимальному беспорядку, то есть максимально независимым возможностям.