（此题永久悬赏1000分，一旦被证实/反驳，将追溯设置并奖励）
（可能重复：https://math.stackexchange.com/questions/4232108/%ce%bbp2-the-calculus-of-constructions-and-quantifying-over-propositions)
考虑 lambda 立方体：
https://en.wikipedia.org/wiki/Lambda_cube
支持类型多态性和依赖类型的类型系统：
- 依赖类型/取决于项的类型：∀ (a: A), B
- 类型多态性/类型类别/术语取决于类型：∃ A, (b: B)
（假设 a,b,c 是项，A,B,C 是类型）
可以归类为系统λP2，是二阶谓词逻辑的一种表现形式。
除此之外，构造微积分 (CoC) 还支持：
- 更高种类/类型构造函数/类型取决于类型：A -> B
它是大多数最强大的证明助手的基础，包括 coq 和 LEAN4。
这种额外的能力似乎是无用的，因为任何此类推论都可以重写为等效的对偶形式：
{ // primary
A -> B
}
{ // dual
∃ A, (g: G)
∀ (g: G), B
}
这里，术语g: G（将被称为通用对象）只是一个中间构造，它携带很少的编译时信息，可以由证明者/编译器动态生成，并且可以在运行时擦除。
那么为什么 CoC（或许多依赖类型系统中的更高级规则）是必要的呢？具体来说：
- CoC 中的每个证明到 λP2 是否存在单射映射？
- 鉴于依赖对象类型（DOT，Scala 3 的底层类型系统）系统是系统 D 的扩展，它类似于 λP2，但将依赖类型限制为路径显式、编译时已知术语，是否存在来自每个 Scala 的单射映射编程为没有更高类型的等效程序？
UPDATE 1
理想情况下，以下示例应在证明助手中形式化，并发布在数学/证明助手堆栈交换下，但我选择使用 Scala 3（一种具有丰富类型系统的函数式语言）编写所有示例，原因如下：
- DOT 和系统 D 都有健全性证明，而更高种类的 DOT 则没有。
- The effort to encode higher kind in Scala 3 in terms of dependent types has been attempted many times before (see the following 2016 slide):
- https://conf.researchr.org/details/scala-2016/scala-2016/5/Implementing-Higher-Kinded-Types-in-Dotty
- https://www.slideshare.net/Odersky/implementing-higherkinded-types-in-dotty
- Scala 3 的现状高级推理实现可能过于复杂，并且是一些错误和歧义的根源（有关详细信息，请参阅错误修复部分）。因此，这个猜想带来了回避它们的直接好处。
- 我不是证明助手的熟练用户，我在数学/证明助手堆栈交换方面也没有足够的声誉来设置赏金。
无论如何，我将尝试在几周内发布 LEAN4 中的改进版本。
执行
在 Scala3 中，临时类型多态性有 2 种表现形式（术语取决于类型）：该术语可以是外部对象：
object Term {
trait TT {def outer = Term.this}
}
或为该类型调用的隐式术语：
trait Support[T]
trait TT
object TT {
implicit lazy val SupportTT: Support[TT] = ???
}
为了简单起见，以下示例将仅使用外部对象。
Examples
使用上面的约定，最简单的不变无界Vec[T]可以映射成TGen#Vec:
（无界不变）
{ // Primary
trait Vec[T]
trait Matrix[T] extends Vec[Vec[T]]
object VInt extends Vec[Int]
object MInt extends Matrix[Int]
}
{ // Dual
trait Vec_* {
type TT
}
{ // Dual
trait Vec_* {
type TT
}
trait TGen {
type T
trait Vec extends Vec_* { type TT = T }
object VecTGen extends TGen { override type T = TGen.this.Vec }
trait Matrix extends VecTGen.Vec
}
object IntGen extends TGen { type T = Int }
object VInt extends IntGen.Vec
object MInt extends IntGen.Matrix
}
与 CoC 不同，DOT 支持子类型，这会带来一些复杂性，其中之一是依赖类型现在变成了界限，即type TT = T只是一个简写type TT >: T <: T。当以下情况时，需要填写完整的表格：Vec[T]有界参数：
（上限和下限不变）
{ // Primary
trait Vec[T >: Nothing <: Any]
trait NVec[T >: Nothing <: Number] extends Vec[T]
}
{ // Dual
trait Vec_*
trait TGen {
type T_/\ <: Any
type T_\/ >: Nothing <: T_/\
trait Vec extends Vec_* { type TT >: T_\/ <: T_/\ }
}
trait NTGen extends TGen {
override type T_/\ <: Number
}
}
...或方差：
（协变）
trait _0
trait _1 extends _0
{ // Covariant: Primary
trait Cov[+T]
type Cov_* = Cov[_]
implicitly[Cov[_1] <:< Cov[_0]]
trait G0 extends Cov[_0]
trait G1 extends G0 with Cov[_1]
object G0 extends G0
object G1 extends G1
}
{ // Dual
trait Cov_* { type TT }
trait TGen {
type T_/\
type T_\/ <: T_/\ // not used
type Cov = Cov_* { type TT <: T_/\ }
}
object _0Gen extends TGen { type T_/\ = _0; trait CovImpl extends Cov_* { type TT <: T_/\ } }
object _1Gen extends TGen { type T_/\ = _1; trait CovImpl extends Cov_* { type TT <: T_/\ } }
// boilerplate can be avoided by allowing trait to extend duck types directly
implicitly[_1Gen.Cov <:< _0Gen.Cov]
trait G0 extends _0Gen.CovImpl
trait G1 extends G0 with _1Gen.CovImpl
object G0 extends G0
object G1 extends G1
}
（逆变）
{ // Similarily, contravariant, Primary
trait Cov[-T]
type Cov_* = Cov[_]
implicitly[Cov[_0] <:< Cov[_1]]
}
{ // Dual
trait Cov_* {
type TT
}
trait TGen {
type T_/\ // not used
type T_\/ <: T_/\
type Cov = Cov_* { type TT >: T_\/ }
}
object _0Gen extends TGen {
type T_/\ = Any
type T_\/ = _0
}
object _1Gen extends TGen {
type T_/\ = Any
type T_\/ = _1
}
implicitly[_0Gen.Cov <:< _1Gen.Cov]
Hindley-Milner/System F 中的常见函数式编程概念也变得更简单，例如：
（带有 Church 编码的自然数）：
trait Nat
trait _1 extends Nat
{ // Primary
trait Succ[N <: Nat] extends Nat
type _4 = Succ[Succ[Succ[_1]]]
}
{ // Dual
trait NGen {
type _N <: Nat
trait Succ extends Nat
}
object _1 extends NGen {
type _N = _1
}
object _2 extends NGen {
type _N = _1.Succ
}
object _3 extends NGen {
type _N = _2.Succ
}
type _4 = _3.Succ
}
（从属多项函数）
{ // Primary
sealed trait Col[V] {
trait Wrapper
val wrapper: Wrapper = ???
}
val polyFn: [C <: Col[?]] => (x: C) => x.Wrapper =
new PolyFunction {
def apply[C <: Col[?]](x: C) = x.wrapper
}
type CC = Col[_]
}
{ // Dual
trait VGen {
type V
sealed trait Col {
trait Wrapper
val wrapper: Wrapper = ???
}
}
val polyFn: [G <: VGen] => (gen: G) =>
[C <: gen.Col] => (x: C) => x.Wrapper
= ???
}
（F-界多态性）
{ // primary
trait Node[T <: Node[T]]
trait NN extends Node[NN]
}
{ // Dual
trait Node_* { type TT }
trait TGen {
type T_/\ <: NodeImpl
type T_\/ <: T_/\
type Node = Node_* { type TT >: T_\/ <: T_/\ }
trait NodeImpl extends Node_* { type TT >: T_\/ <: T_/\ }
}
object NNGen extends TGen {
type T_/\ = NN
type T_\/ = NN
}
trait NN extends NNGen.NodeImpl
}
Bugfixes
Scala3 编译器仍在积极开发中，由于将高级类型与子类型混合的复杂性，引入了一些错误和歧义，它们可能会被回避，甚至以对偶形式被忽视，例如：
（主要文章从类型系统的角度来看，在 Scala 3 中，方差是否会影响类型“F[T]”和“F[_ )
对于 scala 中的协变更高类型Mat[+T]，证明这一点应该是微不足道的Mat[Y <:< X] <:< Mat[X]对全部Y <:< X根据定义，并且Mat[_ <: X] <:< Mat[X]，但此时，Scala3编译器不会承认这一点。
（类型之间的扩展相等F[+T] and F[+_ <: T])
{ // Primary
trait Mat[+T]
summon[Mat[Product] <:< Mat[_ <: Product]]
summon[Mat[_ <: Product] <:< Mat[Product]] // oops
summon[Mat[Product] =:= Mat[_ <: Product]] // oops
}
{ // Dual
trait Mat_* {
type TT
}
trait TGen {
type T_/\
type T_\/ <: T_/\
type Mat = Mat_* { type TT <: T_/\ }
}
object ProductGen extends TGen {
override type T_/\ = Product
override type T_\/ = Product
}
object LessThanProductGen extends TGen {
override type T_/\ = Product
override type T_\/ = Nothing
}
summon[ProductGen.Mat =:= LessThanProductGen.Mat]
}
（主要文章在 Scala 2 或 3 中，是否有不使用匹配类型的更高级参数提取器？)
（该bug已在Scala 3.4.0中修复https://github.com/lampepfl/dotty/issues/17149)
匹配类型是 Scala3 的一个新功能，相当于一个临时类型构造函数，它可以在编译时简化为具体类型。但它的实现是由复杂的宏支持的，在与更高的种类和方差结合时需要仔细处理。同时，早在这个功能存在之前，它的双重形式（使用隐式术语作为类型类）就已经在 Scala2 中用于相同的目的，并且它在任何 Scala 版本中都可以完美地工作。为了保持一致性，以下示例将包括两种双重形式，分别使用隐式术语和外部对象作为类型类：
（匹配类型提取协变参数）
{ // primary
trait Vec[+T]
type Ext[S <: Vec[_]] = S match {
case Vec[t] => t
}
implicitly[Ext[Vec[Int]] =:= Int]
implicitly[Ext[Vec[Int]] <:< Int]
// broken in Scala 3.3: Cannot prove that e.Ext[Seq[Int]] =:= Int
// works in Scala 3.4+
implicitly[Int <:< Ext[Vec[Int]]]
}
{ // dual, type classes are implicit terms
trait Vec[+T]
trait SGen {
type SS
type Ext
}
type GenAux[S] = SGen { type SS = S }
object SGen {
class VecGen extends SGen {
final type SS = Vec[Ext]
}
implicit def forVec[T]: VecGen { type Ext = T } = new VecGen {
type Ext = T
}
}
val gen = summon[GenAux[Vec[Int]]]
summon[gen.Ext =:= Int] // success!
}
{ // dual, type classes are outer objects
trait Vec_* { type TT }
type VecLt[T] = Vec_* { type TT <: T } // This is unnecessary if match type can extract bound directly
trait TGen {
type T_/\
type Vec = Vec_* { type TT <: T_/\ }
}
object IntGen extends TGen {
type T_/\ = Int
}
trait SGen {
type S <: Vec_*
type Ext
}
trait VecGen extends SGen {
val tGen: TGen
type S = tGen.Vec
final type Ext = tGen.T_/\
}
object VecIntGen extends VecGen {
val tGen: IntGen.type = IntGen
}
implicitly[VecIntGen.Ext =:= Int] // success!
{ // If you insist on using match type without higher kind
trait SGen {
type S <: Vec_*
type Ext = S match {
case VecLt[t] => t
case _ => S
}
}
object SIntGen extends SGen {
final type S = Int
}
implicitly[SIntGen.Ext =:= Int]
implicitly[SIntGen.Ext <:< Int]
// still broken in Scala 3.3, but easier to fix
}
}
TL;DR
根据经验，每组类型参数都映射到具有 2x 依赖类型的泛型对象，分别对应于上限和下限。我还没有看到这条规则的反例，而且这篇文章已经变得太长了。要将其合并到 Scala 编译器（或任何使用类似类型系统的编译器）中，需要对其可靠性进行正式证明（当与 λP2、DOT 及其扩展结合使用时）。
所以问题就变成了：证明或反驳它的最现实的路线图是什么，无论是在纸上还是用机器？
UPDATE 2
有人问我这个公式是否可以引入吉拉德悖论，实现类型构造函数的众多复杂问题之一。从我使用编译器的有限经验来看，Scala 在这两种形式上都很好地避免了这种情况：
object Paradox {
{ // Primary
trait Vec[T]
type VV1 = List[Vec] // paradox!
type VV2 = [T] =>> Vec[T]
type NN = List[VV2] // paradox!
}
{ // Dual
trait Vec_* {
type TT
}
trait TGen {
type T
trait Vec extends Vec_* {
type TT = T
}
}
type VV2 = [TT] =>> (TGen { type T = TT })#Vec
type NN = List[VV2] // paradox!
}
}
在所有 3 种情况下，Scala 都给出了相同的错误：Type argument Vec/VV2 does not have the same kind as its bound。这显然不是一个严格和客观的验证，为此我需要对每个矛盾的例子从初级形式到对偶形式进行一致的映射。尽管如此，请指出该表述是否引入了任何以前不存在的悖论。
