Type projection SI-3443にさらっとtype projection: は、 と同値である、と書いてある。一方、言語仕様には しかないようで、コンパイラも にはエラーを出す。 class T { class A } type `_.A` = x.A forSome { val x: T } implicitly[`_.A`

ConstantType Scalaには7.typeのような型(constant type)がこっそり含まれていた。macroで取り出して使うことができる。 object ConstantTypeOf { type apply[T](x: T) = macro impl[T] def impl[T: c.WeakTypeTag](c: Context)(x: c.Expr[T]): c.Tree = { i…

vs. dependent types 一般に、dependent type family: を実装するのは難しい(らしい)。一方、singleton type family: の実装はなんとかなるので、 を満たすことから、 という関係のもと、 Promotion Haskellはすごいことになっており というデータ型があると…

Abstract type member Scalaでは、abstract type memberとtype projectionを使ってtype family を作ることができる。 object PathDepType { trait K { type A // abstract type member } trait a extends K { override type A = Int } trait b extends K { o…

Type family 型族のこと。 つまり、全ての型の集合を とすると なる関数のこと。族の記法を使うと 特に断らない場合は、添字集合 は の部分集合とする。 Dependent type family Dependent type familyとは、添字集合が型になっているtype familyのこと。 つ…

Union, 和集合 集合族 について を と書き、集合族 のunionと呼ぶ。つまり、 Disjoint union 集合族 について を と書き、集合族 のdisjoint unionと呼ぶ。 Coproduct 圏論においては、 の代わりに が使われ、coproductと呼ばれる。 Dependent sum 型理論に…

Cartesian product, 直積 集合族 について、の元の族: が を満たすとき と(個人的に)書く。このような族の集合を、 と書き、集合族 のcartesian productと呼ぶ。つまり、 Dependent product 型理論においては、 の代わりに や が使われる。 特に、型を添字集…