Does Haskell's type system honor the Liskov Substitution Principle?

Question

I'm coming from a Java background, and I'm trying to wrap my head around Haskell's type system. In the Java world, the Liskov Substitution Principle is one of the fundamental rules, and I'm trying to understand if (and if so, how) this is a concept that applies to Haskell as well (please excuse my limited understanding of Haskell, I hope this question even makes sense).

For example, in Java, the common base class Object defines the method boolean equals(Object obj) which is consequently inherited by all Java classes and allows for comparisons like the following:

        String hello = "Hello";
        String world = "World";
        Integer three = 3;

        Boolean a = hello.equals(world);
        Boolean b = world.equals("World");
        Boolean c = three.equals(5);

Unfortunately, due to the Liskov Substitution Principle, a subclass in Java cannot be more restrictive than the base class in terms of what method arguments it accepts, so Java also allows some nonsensical comparisons that can never be true (and can cause very subtle bugs):

        Boolean d = "Hello".equals(5);
        Boolean e = three.equals(hello);

Another unfortunate side effect is that, as Josh Bloch pointed out in Effective Java a long time ago, it is basically impossible to implement the equals method correctly in accordance with its contract in the presence of subtyping (if additional fields are introduced in the subclass, the implementation will violate the symmetry and/or transitivity requirement of the contract).

Now, Haskell's Eq type class is a completely different animal:

Prelude> data Person = Person { firstName :: String, lastName :: String } deriving (Eq)
Prelude> joshua = Person { firstName = "Joshua", lastName = "Bloch"}
Prelude> james = Person { firstName = "James", lastName = "Gosling"}
Prelude> james == james
True
Prelude> james == joshua
False
Prelude> james /= joshua
True

Here, comparisons between objects of different types get rejected with an error:

Prelude> data PersonPlusAge = PersonPlusAge { firstName :: String, lastName :: String, age :: Int } deriving (Eq)
Prelude> james65 = PersonPlusAge {  firstName = "James", lastName = "Gosling", age = 65}
Prelude> james65 == james65
True
Prelude> james65 == james

<interactive>:49:12: error:
    • Couldn't match expected type ‘PersonPlusAge’
                  with actual type ‘Person’
    • In the second argument of ‘(==)’, namely ‘james’
      In the expression: james65 == james
      In an equation for ‘it’: it = james65 == james
Prelude>

While this error intuitively makes a lot more sense than the way Java handles equality, it does seem to suggest that a type class like Eq can be more restrictive with regards to what argument types it allows for methods of subtypes. This appears to violate the LSP, in my mind.

My understanding is that Haskell does not support "subtyping" in the object-oriented sense, but does that also mean that the Liskov Substitution Principle does not apply?

Protoxide

The concept of the Liskov substitution principle is Contravariance in a functional language: typeclasses.com/contravariance fpcomplete.com/blog/2016/11/covariance-contravariance – Dwain

I can't precisely see what the LSP would be in a language without subtyping like Haskell. To me, LSP is mostly about OOP objects, their invariants, and how to make a subclass without breaking the invariants, so that it can substitute the superclass. I can't see how this applies to Haskell. – Bendicty

@WillemVanOnsem I fail to see what you mean by this. As a matter of fact, OO subtyping can be described as covariant polymorphism, which is no doubt some category-theoretical functor thing. But how does the Haskell contravariant-functor class give anywhere comparable functionality? – Antigua

The name “typeclass” is a false friend for folks coming from OOP. They’re meant to be taken literally as “classes of types”, i.e., single-parameter typeclasses in Haskell are sets of types, and a lawful instance is a proof that the type is in the set; multi-parameter classes (MPTCs) are relations on types; and functional dependencies and type families allow functions on types. Subclasses are subsets (or subrelations): class Eq a => Ord a says that if a type is in Ord, then it must also be in Eq, therefore Ord is a subset of Eq. (The => arrow is backward implication.) – Riverside

Answer 1

tl;dr: Haskell's type system not only honors the Liskov Substitution Principle – it enforces it!

---

Now, Haskell's Eq type class is a completely different animal

Yes, and in general type classes are a completely different animal (or meta-animal?) from OO classes. The Liskov Substitution Principle is all about subclasses as subtypes. So first of all a class needs to define a type, which OO classes do (even abstract ones / interfaces, only, for those the values must be in a subclass). But Haskell classes don't do anything like this at all! You can't have a “value of class Eq”. What you actually have is a value of some type, and that type may be an instance of the Eq class. Thus, class semantics are completely detached from value semantics.

Let's formulate that paragraph also as a side-by-side comparison:

• OO: classes contain
  • values (better known as objects^★)
  • subclasses (whose values are also values of the parent class)
• Haskell: classes contain
  • types (known as instances of the class)
  • subclasses (whose instances are also instances of the parent class)

Note that the description of a Haskell class does not even mention values in any way. (As a matter of fact, you can have classes that don't have methods that are concerned with any runtime values at all!)

So, now we've established subclassing in Haskell has nothing to do with values of a subclass, it's clear that the Liskov principle can't even be formulated on that level. You could formulate something similar for types:

• If D is a subclass of C, then any type that's an instance of D can also be used as an instance of C

– which is absolutely true, albeit not really talked about; indeed the compiler enforces this. What it entails is

• In order to write an instance Ord T for you type T, you must first also write an instance Eq T (which would of course be just as valid on its own, irrespective of whether the Ord instance is defined too)
• If the constraint Ord a appears in a function's signature, then the function can automatically also assume that the type a has a valid Eq instance too.

That may not be a really interesting answer to the question of Liskov in Haskell.

Here's something that makes it a bit more interesting though. Did I say Haskell doesn't have subtypes? Well, actually it does! Not plain old Haskell98 types, but universally quantified types.

DON'T PANIC I'll try to explain what that is with an example:

{-# LANGUAGE RankNTypes, UnicodeSyntax #-}

type T = ∀ a . Ord a => a -> a -> Bool
type S = ∀ a . Eq a => a -> a -> Bool

Claim: S is a subtype of T.

–If you've been paying attention then you're probably thinking at this point wait wait wait, that's the wrong way around. After all, Eq is a superclass of Ord, not a subclass.
But no, S is the subtype!

Demonstration:

x :: S
x a b = a==b

y :: T
y = x

The other way around is not possible:

y' :: T
y' a b = a>b

x' :: S
x' = y'

error:
    • Could not deduce (Ord a) arising from a use of ‘y'’
      from the context: Eq a
        bound by the type signature for:
                   x' :: S
      Possible fix:
        add (Ord a) to the context of
          the type signature for:
            x' :: S
    • In the expression: y'
      In an equation for ‘x'’: x' = y'

Properly explaining Rank-2 types / universal quantification would lead a bit too far here, but my point is: Haskell does allow a kind of subtyping, and for it the Liskov Substitution Principle is a mere corollary of the compiler-enforced “LSP” for types in typeclasses.

And that's rather neat, if you ask me.

---

^★_{We don't call values “objects” in Haskell; objects are something different for us, that's why I avoid the term “object” in this post.}

Antigua

Thanks for that comprehensive answer, @leftaroundabout, and also for the intriguing pointer to universally quantified rank-2 types (that one is going to take me a while to digest, though). Would it be fair to say that the LSP, in its original form, at a value/object-level does not make sense in Haskell (due to the separation of value versus class/type semantics), but that an analogous principle can be formulated at the type-level (and that principle is in fact enforced by the Haskell compiler)? – Protoxide

Well, at any rate you can say classes don't induce subtyping and therefore LSP on the value/object level can't have anything to do with class membership. – Antigua

Can I reason that Eq is a "subtype" of Ord because Ord depends on Eq, and so that every Ord will satisfy Eq but not ever Eq will satisfy Ord? – Frisbie

@Frisbie well, I really would say “subtype” only on the resultant universally quantified types. And the reason S is a subtype of T is that is has to quantify over a bigger set of types (thus, values of S need to do everything that values of T need, plus some more namely also quantifying over the non-Ord but Eq types). – Antigua

Your example doesn’t use higher-rank polymorphism, just the “subtyping” of typeclass implication (Ord implies Eq). With higher-rank types, the subtype relation is “more polymorphic than”, and functions are contravariant in their input—e.g., you can pass a more polymorphic argument for a less polymorphic parameter, but not vice versa: given f :: (Int -> Int) -> Int; f x = x 5 and g :: (forall a. a -> a) -> Int; g y = y 5, you can call f id (forall a. a -> a can be “upcasted” to Int -> Int), but not g ((+ 1) :: Int -> Int), since Int -> Int doesn’t work for all types. – Riverside

@JonPurdy good point – the types S and T themselves are only rank-1, just a function using them as parameters is rank-2. – Antigua

I would have mentioned the fact that (lawful) lenses (forall f. Functor f => ...) are (lawful) traversals (forall f. Applicative f => ...) as an example of Haskell enforcing the LSP. – Coburn

Also, I would not conflate the values with objects (in the OOP sense). Objects have a physical identity, which values do not have. – Coburn

The Contravariance/Covariance wikipedia article explains your "Claim: S is a subtype of T." and why it appears the wrong way around (but isn't). There if Cat is a subtype of Animal, then Cat[] is a subtype of Animal[] (covariance). But f :: Animal -> String is a subtype of g :: Cat -> String (contravariance) – Vulcanism