Issues related to possible `HasThisType` implementation in Scala/Dotty


#1

After previous topics related to this thematics:

I have some filling that nice and proper HasThisType-trait implementation is already possible in Scala, and the only thing that I was guessing is still missing - is some sugar around that possible solutions. Actually I have interest to summarize that possible approaches and think about possible improvements.

However when I start trying to encode that possible solution I faced with some issues (some of them are definitely could be treated as bugs, other as enhancements).

So here is a report about my attempts to implement HasThisType and issues that I’ve faced with it.


Specification of This-type (HasThisType trait) which I had in my head cold be formalized as:

  • constraint#1: “.type <: .This”, so that
    if That <: HasThisType then That <: That#This
    (it also includes: this.type <: this.This)

    in particular if val that: That = ... then
    that.type <: that.This

  • constraint#2: “#This#This <: #This” , so that
    if That <: HasThisType then That#This#This <: That#This

    in particular if That <: { def doSmth(): This } and val that: That = ... then
    that.doSmth().doSmth().type <: that.This

To define HasThisType-trait / This-type I’ve started from 3 basic skeletons:

  • approach#1: based on direct abstract type
    trait HasThisType {
      type This
    }
  • approach#2: based on generic parameter
    trait HasThisType[PThis] {
      type This = PThis
    }
  • approach#3: based on indirect abstract type (This-type delegates to outer abstract type definition)
    trait HasThisTypeHolder {
      type PThis
      trait HasThisType {
        type This = PThis
      }
    }

Let’s go through them step by step


Proposal : Abstract `This` type inside every class/trait
#2

Approach#1

looks most attractive, since it allows the most natural use of abstract (base) trait/class, comparing: HasThisType vs HasThisType[_] vs HasThisTypeHolder#HasThisType - first option looks definitely better. However my first concern was, that abstract type can not participate
in self-type statement which could make a problem. Meanwhile implementation of constraint#1 turns out to be even simpler in this case:

    trait HasThisType {
      type This >: this.type
    }

- it is enough to use abstract type upper bound to state that thatInstance.type <: thatInstance.This However implementation of constraint#2 (#This#This <: #This) happen to be more complicated in this case.
In fact it is possible in Scala and it consequently causes run-time failure of Dotty compiler, but it could be expressed with the following snippet

    // this is compileable code in both Scala and Dotty compilers
    type HasThisTypeLoverBounded[PThis] = HasThisType { type This <: PThis }
    trait HasThisType {
      type This <: HasThisTypeLoverBounded[This]
    }

Here type This <: HasThisTypeLoverBounded[This] just means that This#This <: This it may look like
type This <: HasThisType { type This /*is This#This*/ <: This /*is outer/just This*/ } - but this notation is quite invalid since 3-rd occurrence of This is ambiguous.
But introduction of parametrized type alias solves that ambiguity.
So replacing contradictory HasThisType { type This /*is This#This*/ <: This /*is outer/just This*/ }
with type HasThisTypeLoverBounded[PThis] = HasThisType { type This <: PThis }
and then using it as type This <: HasThisTypeLoverBounded[This]
will lead us to aforementioned solution.

Looks like good news - full scale implementation/definition of HasThisType is possible in Scala/Dotty.
Band news appears, when one will try to test this solution …
(complete code here) (also described in issue#5876)

    def testHasThisType(): Unit = {
      val that: HasThisType = null.asInstanceOf[HasThisType]
      // check types
      // constraint#1 - this lines works in Dotty, while fails in Scala
      assert(implicitly[that.type <:< that.This] != null)
      val that1: that.This = that
      // constraint#1 - this lines makes Dotty compiler desperately/infinitely hang (tested on current `master` branch)
      assert(implicitly[that1.This <:< that.This] != null)
      val that2: that1.This = that1 // that
    }

It appears that constraint#1 (.type <: .This) implementation works in both Scala and Dotty, however in Scala proof could not be obtained through implicitly[that.type <:< that.This] (wile it is still visible through possibility of assignments without casts), while in Dotty that part works correctly (from both perspectives).
Meanwhile constraint#2 (#This#This <: #This) implementation makes Dotty compiler infinitely hang (or crash), while Scala compiler could not even prove constraint#1 (.type <: .This) for “next generation of This-type”, in particular presumably valid/safe cast that1 : that1.This brings an error “type mismatch; …”

Bigger example (using HasThisType in Dotty) reveals that things in Dotty are also not so terrible as they might be - it is at lest possible to subclass/instantiate that HasThisType trait (but ony “directly” - making abstract sub class leads to similar Dotty compiler run-time crashes)

Here is that demonstrating snippet, comment `FooLike` related code to make it compile-abe under Dotty (also described in issue#5876)
    type HasThisTypeLoverBounded[PThis] = HasThisType { type This <: PThis }
    trait HasThisType {
      type This >: this.type <: HasThisTypeLoverBounded[This]

      // just for testing purposes
      // inline
      def self(): This = this
    }

    // this code is compile-able in Scala while in Dotty it makes compiler runtime crash (tested on Dotty `master`)
    type FooLikeTypeLoverBounded[PThis] = FooLike { type This <: PThis }
    class FooLike extends HasThisType {
      type This >: this.type <: FooLikeTypeLoverBounded[This]
    }

    // this code is compile-able in both Scala and Dotty compiler
    class Foo extends HasThisType {
      type This = Foo
    }
Bigger snippet reveals that in Scala, at least inside of enclosing class/trait body that approach works as expected (`this.type <: this.This` and `this.type#This#This <: this.type#This`). Briefly it will look like:
    // this code is compile-able in Scala while in Dotty it makes compiler runtime crash
    type FooLikeTypeLoverBounded[PThis] = FooLike { type This <: PThis }
    abstract class FooLike extends HasThisType {
      type This >: this.type <: FooLikeTypeLoverBounded[This]

      def doSmth(): This
      def doSmth2(): This = self().doSmth().doSmth()

      def applySmth(arg: This): This
      def applySmth2(arg: This): This = /*doSmth2().*/applySmth(arg.doSmth2()).doSmth2()

    }

    case class Foo(any: Any) extends FooLike {
      type This = Foo

      override def doSmth(): This = Foo(s"doSmth($this)")
      override def applySmth(arg: This): This = Foo(s"($this)applySmth($arg)")
    }

So in general it looks that once/if that Dotty compiler run-time crashes will be fixed one may expect full scale HasThisType definition become possible in new versions of Scala


Approach#2

looks like most conventional way of HasThisType encoding
Final version of that code may look like

    // works in Dotty, in Scala `HasThisType[_ <: PThis]` makes problem, invariant form is available: `HasThisType[PThis]`
    trait HasThisType[PThis <: HasThisType[_ <: PThis]] {
      this: This =>
      type This = PThis

      // inline
      def self(): This with this.type = this
    }

Forcibly covariant version which also works in Scala could look like

    // so that covariant form in Scala may look like following:
    type HasThisTypeBounded[PThis] = HasThisType[_ <: PThis]
    trait HasThisType[PThis <: HasThisTypeBounded[PThis]] {
      this: PThis =>
      type This = PThis

      // this `def` is invalid in Scala
      // def self(): This with this.type = this
    }

Here constraint#2 (#This#This <: #This) defined more or less straightforward. From the first glance it looks more natural to state it as

`PThis <: HasThisType[PThis]` - but this (invariant) constraint is ingeneral un-reasonably tight

(it will encode something like #This#This =:= #This while that.doSmth().doSmth().type <: that.This does not require that tight constraints, unless you want to do something like that.doSmth(that).doSmth(that) assuming that that: That and That <: HasThisType { def doSmth(arg: This): This })

But regarding constraint#1 (.type <: .This) this solution has general problem - in particular it is easily available inside appropriate class like this.type <: this.This, but it is really hard (couple of issues occurs) to make that constraint explicitly/deliberately visible in “outside world”. In particular my understanding of “self-types” make me think about them as of some “abstract protected extends” construct (so when I see trait Foo{ this: Bar => } in my head I just convert it to trait Foo extends protected abstract Bar {}) but when I was trying to “override” that visibility from protected to something like public I had faced facing with “hard resistance” of Scala/Dotty compiler :smile:. (see issue#5879, issue#5878, issue#5880)

In particular, it is possible to reveal that.type <: that.This using aforementioned .self() method like that.self().type <: that.Type see this snippet for demonstrations

By the way, one may try to fix aforementioned snippet by trying to rewrite generic method heading from

      def testSelf[PThis <: HasThisType[_ <: PThis]](that: HasThisType[PThis]): Unit

to

      def testSelf[PThis <: HasThisType[_ <: PThis]](that: PThis with HasThisType[PThis]): Unit

- but this cause even bigger problem to Dotty compiler (it ends up with run-time crash issue#5877), when that signature is tried to accept argument of wildcard type HasThisType[_] of passed parameter see this snippet for demonstration (further rewrites of that snippet may let one to understand that problem there is “activated” by “quasi covariance”(aka use site variance) _ <: T together with recursive generics)

However it would be still interesting to “reveal” that that.type <: that.This relationship directly (interesting at lest from theoretical perspective)
To do so, one may write some code like

    // `This`-type lover boundary proof
    trait HasThisBase[PThis <: HasThisBase[_ <: PThis]] {
      this: PThis =>
      type This >: this.type <: PThis
    }
    trait HasThisType[PThis <: HasThisType[_ <: PThis]] extends HasThisBase[PThis] {
      this: PThis =>
      type This = PThis

      // inline
      def self(): This with this.type = this
    }

Other code which demonstrate the problems with <: transitiveness may look like this (complete example here)

    trait HasThisType[PThis <: HasThisType[_ <: PThis]] {
      this: PThis =>
      // `This`-type lover boundary proof - states that it could be `ThisB` between `this.type <: ThisB <: This`
      type ThisB >: this.type <: This
      type This = PThis
    }

It looks like first part (HasThisBase[_]) could be enough, but that does not provide guaranties for #This#This <: #This, since for base type (HasThisBase) it only provides #This <: #PThis amd #This#This <: #PThis but #PThis <: #This is still missing to complete that chaim and provide #This#This <: #PThis <: #This (so that type This = PThis does that final step).

Once that snippet is written one may expect that now “we got that final solution”. But unfortunately it does not work as expected and only disclose Dotty/Scala compiler problem with <: - transitiveness (A <: B and B <: C here does not mean that A <: C will be inferred automatically) see complete demonstrating example here, alternative rewritten is available for Scala (using invariant PThis-parameter)
(also this problem described in issues: issue#5879, issue#5878)


Approach#3

is some sort of combination of approach#1 and approach#2.
Code that met constraint#2 (#This#This <: #This) and partially met constraint#1 (.type <: .This) (only in form of this.type <: this.This and only inside sub-class/sub-trait body) could look like this
(full version with test here)

    // this code works as expected with both Scala and Dotty compilers
    trait HasThisTypeHolder {
      // `PThis` serves as generic parameter replacement to make usage in sub-classes bit easier
      type PThis <: HasThisType

      trait HasThisType {
        this: PThis =>
        type This = PThis

        // inline
        def self(): This with this.type = this
      }
    }

Again it is possible to make attempt to fully met constraint#1 (.type <: .This) as

    trait HasThisTypeHolder {
      // `PThis` serves as generic parameter replacement to make usage in sub classes bit easier
      type PThis <: HasThisType

      // `This`-type upper boundary proof
      trait HasThisBase[PThis2] {
        this: PThis2 =>
        type This >: this.type <: PThis2
      }

      trait HasThisType extends HasThisBase[PThis] {
        this: PThis =>
        type This = PThis

        // inline
        def self(): This with this.type = this
      }
    }

And again, unfortunately this only discloses problem with transitiveness of <:, which cold be express with some test similar to previous one

Even simple code which could demonstrate that problems with <: transitiveness could be based on following code (complete example here)

    trait HasThisTypeHolder {
      // `PThis` serves as generic parameter replacement to make usage in sub classes bit easier
      type PThis <: HasThisType

      trait HasThisType {
        this: PThis =>
        type This = PThis

        // `This`-type lover boundary proof - states that it could be `ThisB` between `this.type <: ThisB <: This`
        type ThisB >: this.type <: This

        // inline
        def self(): This with this.type = this
      }
    }

(also this problem is described in issues: issue#5879, issue#5878)


#3

Also in previous posts (1, 2) where highlighted possible need of some ThisLikeN[T1,...TN]-types (HasThisLikeTypeN traits). Actually approach#1 could not be used here (constraint this.type <: this.ThisLike[T1,...Tn] could not be achieved with regular abstract types, only self-types could provide that in this case).
Meanwhile approach#2 and approach#3 could be easily adapted to this use case.

So starting from this basic skeletons

    trait HasThisType1[PThisLike1[_], T1] {
      type ThisLike1[P1] = PThisLike1[P1]
    }
    trait HasThisTypeHolder {
      type PThisLike1[_]
      trait HasThisType1[T1] {
        type ThisLike1[P1] = PThisLike1[P1]
      }
    }

final implementations may look like described below.


Approach#2

applied to HasThisLikeN / ThisLike[T1, ... ,TN] could look like this

    // covariant version
    trait HasThisType1[PThisLike1[P1] <: HasThisType1[_ <: PThisLike1, P1], T1] {
      this: PThisLike1[T1] =>
      type ThisLike1[P1] = PThisLike1[P1]

      inline
      def self(): ThisLike1[T1] with this.type = this
    }

    trait HasThisType2[PThisLike2[P1,P2] <: HasThisType2[_ <: PThisLike2, P1, P2], T1,T2] {
      this: PThisLike2[T1,T2] =>
      type ThisLike2[P1,P2] = PThisLike2[P1,P2]

      inline
      def self(): ThisLike2[T1,T2] with this.type = this
    }

Invariant version (with stronger constraint like #PThisLike1#PThisLike1 =:= #PThisLike1) will become

    // invariant version
    trait HasThisType1[PThisLike1[P1] <: HasThisType1[PThisLike1, P1], T1] {
      this: PThisLike1[T1] =>
      type ThisLike1[P1] = PThisLike1[P1]

      // inline
      def self(): ThisLike1[T1] with this.type = this
    }

    trait HasThisType2[PThisLike2[P1,P2] <: HasThisType2[PThisLike2, P1, P2], T1,T2] {
      this: PThisLike2[T1,T2] =>
      type ThisLike2[P1,P2] = PThisLike2[P1,P2]

      // inline
      def self(): ThisLike2[T1,T2] with this.type = this
    }

Again constraint#1 (.type <: .ThisLike1[T1]) and constraint#2 (#ThisLike1[_]#ThisLike1[P1] <: #ThisLike1[P1]) could be easily seen inside class/trait body
(like this.type <: this.ThisLike1[T1], etc), while outside constraint#1 could be exposed through that.self().type <: that.ThisLike[T1] (where that: HasThisType1[T1]), or again alternatively one may define auxiliary type type ThisLikeB <: this.type <: ThisLike1[T1] and expose that as that.type <: that.ThisLikeB <: ThisLike1[T1]
(complete example here) (see also issue#5878, issue#5879)

Bigger snippet that reveals that in Scala, at least inside of enclosing class/trait body that approach works as expected (`this.type <: this.ThisLike1[T1]` and `this.type#ThisLike1[_]#ThisLike1[P1] <: this.type#ThisLike1[P1]`). Briefly it will look like:
    trait FooLike[PFooLike[P1] <: FooLike[PFooLike, P1], T1] extends HasThisType1[PFooLike, T1] {
      this: PFooLike[T1] =>

      def doSmth(): ThisLike1[T1]
      def doSmth2(): ThisLike1[T1] = self().doSmth().doSmth()

      def applySmth[P1](arg: ThisLike1[P1]): ThisLike1[P1]
      def applySmth2[P1](arg: ThisLike1[P1]): ThisLike1[P1] = doSmth2().applySmth(arg.doSmth2()).doSmth2()

    }

    case class Foo[T1](any: Any, tag: T1) extends FooLike[Foo,T1] {

      override def doSmth(): ThisLike1[T1] = Foo(s"doSmth($this)", tag)
      override def applySmth[P1](arg: ThisLike1[P1]): ThisLike1[P1] = Foo(s"($this)applySmth($arg)", arg.tag)
    }

Approach#3

applied to HasThisLikeN / ThisLike[T1, ... ,TN] could look like this

    trait HasThisTypeHolder {
      // `PThisLike1` serves as generic parameter replacement to make usage in sub classes bit easier
      type PThisLike1[P1] <: HasThisLikeType1[P1]

      trait HasThisLikeType1[T1] {
        this: PThisLike1[T1] =>

        type ThisLike1[P1] = PThisLike1[P1]

        // inline
        def self(): ThisLike1[T1] with this.type = this
      }

      // `PThisLike2` serves as generic parameter replacement to make usage in sub classes bit easier
      type PThisLike2[P1,P2] <: HasThisLikeType2[P1,P2]

      trait HasThisLikeType2[T1,T2] {
        this: PThisLike2[T1,T2] =>

        type ThisLike2[P1,P2] = PThisLike2[P1,P2]

        // inline
        def self(): ThisLike2[T1,T2] with this.type = this
      }
    }
Bigger snippet that reveals that in Scala, at least inside of enclosing class/trait body that approach works as expected (`this.type <: this.ThisLike1[T1]` and `this.type#ThisLike1[_]#ThisLike1[P1] <: this.type#ThisLike1[P1]`). Briefly will look like snippet inside
    trait FooLikeHolder extends HasThisTypeHolder {
      type PThisLike1[P1] <: FooLike[P1]

      type PFooLike[P1] = PThisLike1[P1]

      trait FooLike[T1] extends HasThisLikeType1[T1] {
        this: PThisLike1[T1] =>

        def doSmth(): ThisLike1[T1]
        def doSmth2(): ThisLike1[T1] = self().doSmth().doSmth()
        def applySmth[P1](arg: ThisLike1[P1]): ThisLike1[P1]
        def applySmth2[P1](arg: ThisLike1[P1]): ThisLike1[P1] = doSmth2().applySmth(arg.doSmth2()).doSmth2()
      }
    }

    object fooHolder extends FooLikeHolder {
      type PThisLike1[P1] = Foo[P1]

      case class Foo[T1](any: Any, tag: T1) extends FooLike[T1] {

        override def doSmth(): ThisLike1[T1] = Foo(s"doSmth($this)", tag)
        override def applySmth[P1](arg: ThisLike1[P1]): ThisLike1[P1] = Foo(s"($this)applySmth($arg)", arg.tag)
      }
    }