PS

Type projection

定義 Scala Dependent type

Type projection

SI-3443にさらっとtype projection:

  • T \text{#} A

は、

  • \exists _ {x \in T}\ x.A
    • \approx \lbrace a \mid {} ^ \exists x \in T, a \in x.A \rbrace

と同値である、と書いてある。一方、言語仕様には

  • \exists _ {x \in T}\ x.A \subseteq T \text{#} A

しかないようで、コンパイラも \supseteq にはエラーを出す。

    class T {
        class A
    }

    type `_.A` = x.A forSome { val x: T }

    implicitly[`_.A` <:< T#A] // ok
    implicitly[T#A <:< `_.A`] // error

参考文献