Let's derive the Liskov Substition Principle from first principles to unify subtyping with the conjunctive and disjunctive operations over (a.k.a. "conjunctivity" and "disjunctivity" of) sets, i.e. everything not outside any (a.k.a. intersection) of and inside all (a.k.a. union) of the sets respectively.
A supertype is the disjunction of its subtypes and a subtype is the conjunction of its supertypes. Profound.
We can't assign the subtype's TYPE to the supertype's TYPE (nor vice versa) because a disjunction is not equivalent to a conjunction.
A supertype is also the conjunction of the subtype variants for each named (i.e. nominal type of) member (i.e. operations a.k.a. methods), because each method implicitly (not Scala's implicit keyword) includes a `this` parameter-- don't conflate this with holding an INSTANCE of the TYPE as this sentence relates types not instances. Thus if our typesystem allows refering to an instance of a subtype with a supertyped reference because the system does not allow invoking methods without a downcast to the required subtype for the `this` of the method, then we can assign instances of subtypes to supertyped references.
In abstract type theory, the type of the `this` parameter for each of the supertype's methods is a disjunction of all the subtypes wherein the method returns the uninstantiable bottom type (e.g. `Nothing` in Scala) if the method is undefined for a subtype. Due to (the membership rule) being conditioned on the enclosing type in this way, the "conjunctivity" and "disjunctivity" (thus the requirement for covariance or contravariance) transpose on each enclosing step starting from the nominal (name of the) type, to the (function a.k.a. method or type parameter) members, to the types of the (function or type) parameters of the members, to the types of the (function or type) parameters of the types of the (function or type) parameters of the members, and so on recursively.
The relationship with covariance is consistent with either dual of De Morgan's laws e.g. one of the duals states the conjunction of all methods for subtypes A and B = not((not A) disjunction (not B)) where inverting the covariance (between co <--> contra) is equivalent to not in this formation, thus subparameters are the inverted covariance requirement of the disjunction of the inverted covariance requirements of the subsubparameters, and so on recursively. The post derives from prior discussion about a union type and Adriaan Moors explanatoin of potential new typing engine for a future Scala:
A subtype is also the disjunction of the subtype variants for each named member (i.e. operations a.k.a. methods) of its supertypes which are unimplemented (i.e. undefined), because the type of the `this` parameter for the unimplemented supertype's methods is the conjunction of all subtypes of the supertypes. This applies to unimplemented inherited methods in abstract types, interfaces, and the bottom type (e.g. `Nothing` in Scala).
Methods can return (assign from) conjunctions and input (assign to) disjunctions of a covariant member, or vice versa for a contraviant member, because we can assign covariantly from conjunctions e.g. val t: A = new (A with B) but not vice versa e.g. val t: A with B = new A. Similarly for disjunctions e.g. val t:Any = new A but not e.g. val t:A = new Any, where I am forced to write Any (the disjunction of every type in the universe, i.e. the top type) in my example because Scala doesn't have a first-class disjunction.
Thus as Luc Duponcheel wrote upthread, subtyping introduces the tradeoff that types can return covariant members and input contravariant members-- or both only for invariant members. Thus covariant type parametrized collections (e.g. List[+A] in Scala) can't enforce criteria w.r.t to the covariant member e.g. force appended elements to be subtypes of the covariant type parameter, e.g. A:
class List[+A](head: A, tail: List[A]) {
def append[B <: A](el: B) = new List(el, this)
}
error: covariant type A occurs in contravariant position in type >: Nothing <: A of type B
def append[B <: A](el: B) = new List(el, this)
^
So they must be allowed to be subtypes:
class List[+A](head: A, tail: List[A]) {
def append[B >: A](el: B) = new List(el, this)
}
defined class List
Yet that tradeoff doesn't apply if the restriction on the type parameter itself:
class List[+A <: C, C](head: A, tail: List[A,C]) {
def append[B <: C](el: B) = new List(el, this)
}
defined class List
Type classes are a form of polymorphism (i.e. extensibility) where the `this` parameter is a type parameter of the operations. The operations for a concrete type can be matched nominally (by name) as shown in the OP or even structurally (although this can be erased and sometime cause reflection on the JVM and thus is probably inefficient).
As Daniel Sobral et. al wrote upthread, distinguish the model (e.g. Applicative or Monad) from the type of polymorphism (subtyping or type classes) employed to accomplish the model. For example, I believe I have shown how to combine subtyping and typeclasses to implement those models:
As for the aforementioned tradeoff Luc Duponcheel wrote about, the model can be a criteria of membership and I am not sure if such a tradeoff ultimately exists. It seems to be always about raising the semantic abstraction to another level that paradigm shifts away the limitation. So more power to the models since they are obviously orthogonal to thus high-level semantics than the choice of polymorphism! By high-level, I measuring the relative distance of semantics from the imperative towards the declarative:
The lower number of votes compared to my other very popular answer on that question, indicates most don't really grasp it or the relevance yet (or that I am wrong).