Search code examples
scalascala-3

Why does a self annotated trait is not assignable to the type of self?

trait Base

trait Plugin { base: Base =>
    def asBase: Base & Plugin = this
}

class Mix extends Base, Plugin

val plug: Plugin = new Mix
val baseA: Base= plug.asBase
val baseB: Base = plug // snorts with "Found: Plugin. Required: Base

Why? If I am correct, the Liskov substitution principle is complied because all instances of Plugin are of a concrete type that is a mix that include a subtype of Base. Therefore, objects of type Basecan be replaced with objects of type Plugin without affecting the correctness of the program.

Solution

  • Liskov principle says

    https://en.wikipedia.org/wiki/Liskov_substitution_principle

    Subtype Requirement: Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T.

    Preconditions cannot be strengthened in the subtype.

    Postconditions cannot be weakened in the subtype.

    Invariants must be preserved in the subtype.

    Liskov principle is about subtyping. Liskov principle is now not applicable because Plugin is not a subtype of Base

    implicitly[Plugin <:< Base] // doesn't compile

    (<:< is weaker than <: https://stackoverflow.com/a/75762663/5249621 but this is ok for us; if Plugin were a subtype of Base i.e. Plugin <: Base then moreover implicitly[Plugin <:< Base] would be).

    I guess you're confusing either trait Plugin { base: Base => } with trait Plugin extends Base or subclasses (inheritance) with subtypes

    What is the difference between a class and a type in Scala (and Java)?

    What is the difference between Type and Class?

    https://typelevel.org/blog/2017/02/13/more-types-than-classes.html

    How to distinguish parameteric types?

    What is a difference between refinement type and anonymous subclass in Scala 3?

    trait Plugin extends Base means that Plugin is a subclass of Base. In particular, this means that Plugin is a subtype of Base, so all subtypes of Plugin are subtypes of Base. But trait Plugin { base: Base => } means that all subclasses of Plugin must be subclasses of Base. This doesn't mean that all subtypes of Plugin must be subtypes of Base (moreover, this doesn't mean that Plugin is a subtype of Base). Indeed, it's easy to declare a type

    type SubPlugin <: Plugin

    which is not a subtype of Base

    implicitly[SubPlugin <:< Base] // doesn't compile

    all instances of Plugin are of a concrete type that is a mix that include a subtype of Base.

    Even if it's true that all values (OOP instances) of Plugin are values (instances) of Base this doesn't make Plugin a subtype of Base and this doesn't mean that all terms of type Plugin are terms of type Base. For example the term x in val x: Plugin = ??? is not a term of type Base.

    You shouldn't think of a type as (only) a set of all values of the type (especially this becomes important in type-level programming where values are not so interesting at all). Sets can be a model (in logical sense: https://en.wikipedia.org/wiki/Model_theory) for types. But sets and types are different

    https://cs.stackexchange.com/questions/91330/what-exactly-is-the-semantic-difference-between-set-and-type

    https://math.stackexchange.com/questions/489369/difference-between-a-type-and-a-set

    https://planetmath.org/11typetheoryversussettheory

    For example if we define two abstract types

    type A

type B

    then there are no values of these types. So these sets would be equal in set-theoretic sense (an empty set). But these types are different. In homotopy type theory (HoTT, https://en.wikipedia.org/wiki/Homotopy_type_theory) 1 = 2 and 1 = 3 are two types without any values but two different types.

    Therefore, objects of type Base can be replaced with objects of type Plugin without affecting the correctness of the program.

    There are always programs that can't fail at runtime but that are rejected at compile time. For example if true then 1 else "a" can't fail at runtime but can be rejected by a language without subtyping e.g. Haskell (but not by Scala which thinks that this is Any). Scala rejects val x: Int = if (true) 1 else "a" although this can't fail at runtime either. Rich enough type system can't be sound and complete at the same time. Normally soundness is preferred over completeness

    What is a sound programming language?

    https://math.stackexchange.com/questions/105575/what-is-the-difference-between-completeness-and-soundness-in-first-order-logic

    You may ask why wouldn't always trait Plugin { base: Base => } mean the same as trait Plugin extends Base. Well, this was design decision of Scala type-system creators. In particular, if this would be the same then two different traits trait A {this: B =>}, trait B {this: A =>} would have the same type.

    Also in trait Plugin extends Base, Base must be a class/trait. But in trait Plugin { base: Base => }, Base can be a type.

    Why scala self type is not a subtype of its requirement

    What is the difference between self-types and trait subclasses?

    Difference between trait inheritance and self type annotation

    What is more Scala idiomatic: trait TraitA extends TraitB or trait TraitA { self: TraitB => }