本帖最后由 yuxuanchiadm 于 2019-7-25 05:50 编辑

【索引贴】https://www.mcbbs.net/thread-887515-1-1.html

类型层级

在Scala中，Any是整个类型层级的顶类型（Top Type），Nothing是整个类型层级的底类型（Bottom Type）。对于任何类型T，以下子类型关系存在：
Nothing类型的值可以转换为任意类型的值，处于类型层级的底端，所以称其为底类型。任意类型的值都可以转换为Any类型的值，处于类型层级的顶端，所以称其为顶类型。需要注意的是即使Nothing类型的值可以转换为任意类型的值，但是Nothing类型本身是没有任何值的。如果一个值是引用类型，那么AnyRef是其父类，Null是其子类。Null类型只有一个值null，也就是说无法将其他除Nothing类型以外的值转换到Null类型。对于任何引用类型T，以下子类型关系存在：
对于数值类型、Boolean以及Unit，AnyVal是其父类：

柯里霍华德同构

柯里霍华德同构（Curry–Howard Isomorphism）指的是类型与命题、程序与证明的对应关系，由其发展出的类型论（Type Theory）这一数学分支对函数式编程的相关研究有很大的影响。在Scala的类型系统中，对于下列类型：

• 底类型（Bottom Type）对应逻辑假（Logical Falsity）
• 单位类型（Unit Type）对应逻辑真（Logical Truth）
• 和类型（Sum Type）对应逻辑析取（Logical Disjunction）
• 积类型（Product Type）对应逻辑合取（Logical Conjunction）
• 函数类型（Function Type）对应逻辑蕴含（Logical Implication）
  

另外，如果一个编程语言支持依赖类型（Dependent Type），那么其类型系统对应了高阶谓词逻辑（Higher Order Predicate Logic），对于下列类型：

• 依赖和类型（Dependent Sum Type、Sigma Type）对应存在量化（Existential Quantification）
• 依赖积类型（Dependent Product Type、Pi Type）对应全称量化（Universal Quantification）
  

Scala并不直接支持依赖类型，但是其支持的参数化多态（Parametric Polymorphism）以及类型构造器（Type Constructor）也就是常说的泛型，粗略来（不考虑Subtyping以及一些Edge case）说，其类型系统对应了高阶命题逻辑（Higher Order Proposition Logic）。需要注意的是，在高阶命题逻辑中能量化的只有命题。不存在谓词，也就是不存在从值到类型的函数，也不能对值进行量化。对于一些特殊的类型：

• 顶类型（Top Type）对应了：forall a. a
• 多态函数类型（Polymorphic Method Type）对应了全称量化
• 存在类型（Existential Type）对应了存在量化（将要在Dotty，也就是Scala3中废除）