2 ms·

apparently LSP is just a contravariant functor https://apocalisp.wordpress.com/2010/10/06/liskov-substitution-principle-is-contravariance/ https://apocalisp.wor

• tel 12y ago
  The trick of that article is noting that Rúnar translates "S is a subtype of T" to "S => T", e.g. subtyping implies coercion. This is the first part of subtyping. The second part is that we must have that definitions of Q[S] for any Q must follow naturally from definitions of Q[T]. So let's say that Apple is a subtype of Fruit. That means that there exists a natural coercion function f : Apple => Fruit. It also means that if we have a predicate Delicious that we define for both Fruit and Apple then the answer Delicious[Apple] must be exactly Delicious[Fruit].comap(f). If they don't align then your coercion function is somehow wrong and not implementing subtyping properly.