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?

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.}